Commits

Paweł Wieczorek  committed 8b01b63

The _S case is finished

  • Participants
  • Parent commits 6989058
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

 
 (* SECOND CASE *)
 
-admit.
-
+exists (DupN (DneS e)).
+split.
+unfold Dup.
+simpl.
+eapply appNeS.
+split.
+replace (DupN (DneS e)) with (Dup Dnat (DneS e)); auto.
+eapply Reflect_Characterization.
+eauto.
+eauto.
+constructor 1.
+intros.
+clear_inversion Hda.
+clear_inversion H8.
+edestruct H6 as [ne [Hne Hne']].
+eexists.
+split.
+eauto.
+eauto.
+split.
+
+(**)
+
+eapply EQ_TP_SB_NAT.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+(**)
+
+intros.
+ 
+
+assert ( Delta0 |-- a : TmSb TmNat (Sups i))  as Ha.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert ( Delta0 |-- a : TmNat ) as Ha'.
+eapply CONV.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+assert ( Delta0 |-- a : TmSb TmNat Sid ) as Ha''.
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+move Ha'' after Ha'.
+
+
+assert ( Delta0,, TmNat  |-- [Sext (Sseq (Sseq SB (Sups i)) Sup) TmVar ] : Gamma,, TmNat ) as Hsb.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+generalize dependent HDnat.
+cut (Dnat = Dnat); auto.
+cut (Dnat = Dnat); auto.
+generalize Dnat at 1 5 8 as d0.
+generalize Dnat at 2 4 6  as d1.
+intros.
+destruct HDnat; clear_inversion H5.
+simpl in H9.
+destruct H9.
+destruct H9.
+
+(**)
+
+specialize (H10 _  _ H6).
+destruct H10 as [ve].
+destruct H10.
+
+clear_inversion H10.
+
+exists (TmApp TmS ve).
+
+split.
+unfold Ddown; simpl.
+eapply reifyNf_ne.
+eauto.
+
+(**)
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_CONG_SB.
+eapply EQ_SB_REFL.
+eauto.
+
+eapply EQ_CONG_FUN_E.
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+unfold TmArr.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+eapply Ha''.
+
+(**)
+
+eapply SB_F.
+eauto.
+eauto.
+
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SSEQ.
+eauto.
+eapply SEXT.
+eauto.
+eauto.
+
+eauto.
+eauto.
+eauto.
+
+(**)
+   
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SSEQ.
+eapply SSEQ.
+eauto.
+eapply SEXT.
+eauto.
+eauto.
+
+eauto.
+
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+
+eapply SSEQ.
+eapply SSEQ.
+eapply SSEQ.
+eauto.
+eapply SEXT.
+eauto.
+eauto.
+
+eauto.
+
+eauto.
+eauto.
+
+(***)
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_SBAPP.
+
+(* OLD *)
+eauto.
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+
+unfold TmArr.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply System.SB.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply System.SB.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eapply SSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply System.SB.
+eauto.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+unfold TmArr.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+eapply EQ_CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SSEQ.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+
+(**)
+
+eapply SSEQ.
+eapply SSEQ.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+
+eapply EQ_CONV.
+eapply EQ_SBNATS.
+eauto.
+
+unfold TmArr.
+eapply EQ_TP_REFL.
+eauto.
+
+eapply EQ_REFL.
+eauto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
 Qed.
 
 
+
 Theorem Rel_Fundamental_Absurd: forall Gamma A Delta SB denv DT DT' (HDT : DT === DT' #in# PerType) dt,
   Gamma |-- A ->
   (forall (Delta : Cxt) (SB : Sb) (denv : DEnv),