Commits

Paweł Wieczorek committed fbd10d0

minor

  • Participants
  • Parent commits e6f2e36
  • Branches another_weird_rule

Comments (0)

Files changed (1)

Nbe/Model/LogRelTm.v

 assert (Gamma,,A ||- TmSb A (Sups 1) #in# HDA) as HDAliftA by (eapply RelTypeLifting; eauto).
 
 assert (Gamma,,A ||- TmVar : TmSb A (Sups 1) #aeq# Dup DA var #in# HDA) as Ha.
-specialize (IHHDT2 (Gamma,,A) (TmSb A (Sups 1)) HDAliftA).
+set (IHHDT3 := IHHDT2).
+specialize IHHDT3.
+specialize (IHHDT2 (Gamma,,A) (TmSb A (Sups 1)) HDAliftA). 
 destruct IHHDT2 as [HI1' [HI2' HI3']].
 specialize (HI3' TmVar var HvarNe).
 apply HI3'.
 eauto.
 
 move HS3 at bottom.
+
+assert (CxtShift (Gamma,,NFA) 1 Gamma) as HCxtShift1'.
+red.
+simpl.
+eapply SSEQ.
+eauto.
+eauto.
+
 specialize (HS3 (Gamma,,A) 1 TmVar dv DB DB' PDA HPDA). 
 specialize (HS3 HdvPDA Happ Happ' HCxtShift1 Ha).
 
 
 destruct H as [HF1 [HF2 HF3]].
 destruct HF1 as [NFF [HF1' HF1'']].
-set (NT := TmFun NFA NFF).
+set (NT := TmFun NFA NFF). 
 exists NT.
 split.
 apply reifyNf_fun with DB.
 eauto.
 *)
 
-assert (Gamma |-- TmFun A F).
+assert (Gamma |-- TmFun A F) as HZZ1.
 eauto.
-clear_inversion H.
+
+clear_inversion HZZ1.
 auto.
-
-
-assert (Gamma,,A |-- TmSb F (Sext (Sups 1) TmVar) === F).
+ 
+
+assert (Gamma,,A |-- TmSb F (Sext (Sups 1) TmVar) === F) as HZZ2.
 eapply EQ_TP_TRANS.
 eapply EQ_TP_CONG_SB.
 eapply EQ_SB_SYM.
 auto.
 apply EQ_TP_SBID.
 auto.
+
+(**)
  
 move NFA at bottom.
 move NFF at bottom.
- 
+  
 eapply EQ_TP_TRANS.
 eauto.
 eapply EQ_TP_CONG_FUN.
 auto.
+
+(**)
+
 eapply EQ_TP_TRANS.
 eapply EQ_TP_SYM.
 eauto.
 auto.
 
+(**)
+
+(*
+assert (Gamma,,NFA |-- TmSb F (Sext (Sups 1) TmVar) === F) as HZZ3.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+simpl.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDSUP.
+eauto.
+eapply EQ_SB_CONG_SEXT.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+eapply EQ_TP_REFL.
+auto.
+
+apply EQ_TP_SBID.
+auto.
+
+
+
 admit.
+*)
+
 
 (*Dfun b) *)