Commits

Paweł Wieczorek  committed c5c09ae

almost finished _Abs case in fundamental lemma - doing equation on terms

  • Participants
  • Parent commits 29a2f34
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

 
 
 assert (Delta0 |-- TmApp (TmSb (TmSb (TmAbs A M) SB) (Sups i)) a ===  TmSb M (Sext (Sseq SB (Sups i)) a) : TmSb (TmSb B (Sext (Sseq SB Sup) TmVar)) (Sext (Sups i) a)) as HYY11.
+
+assert (Delta0 |-- a : TmSb (TmSb A (Sseq SB (Sups i))) Sid) as HZZ1.
+eapply CONV.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto. 
+
+
+assert ( Delta0,, TmSb A (Sseq SB (Sups i)) |-- TmVar
+   : TmSb A (Sseq (Sseq SB (Sups i)) Sup)) as HZZ2.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 |-- a : TmSb A (Sseq SB (Sups i))) as HZZ3.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+
+
+assert (Delta0 |-- [Sseq (Sseq SB Sup) (Sext (Sups i) a)] === [Sseq SB (Sups i)] : Gamma ) as HZZ4.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eauto.
+
+
+assert (Delta0 |--  [Sseq (Sseq (Sseq SB (Sups i)) Sup) (Sext Sid a)]===
+   [Sseq SB (Sups i)]:Gamma) as HZZ5.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eapply SEXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+eapply EQ_SB_REFL.
+eauto.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDR.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+
+
+assert (
+  Delta0
+   |-- TmSb B (Sseq (Sext (Sseq (Sseq SB (Sups i)) Sup) TmVar) (Sext Sid a)) ===
+   TmSb (TmSb B (Sext (Sseq (Sseq SB (Sups i)) Sup) TmVar)) (Sext Sid a)
+) as HZZ6.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+auto.
+eauto.
+(**)
+
 eapply EQ_CONV.
 eapply EQ_TRANS.
 eapply EQ_CONG_FUN_E.
 eauto.
 eauto.
 eapply EQ_REFL.
-eapply RelTerm_implies_WtTm.
-eauto.
+auto.
 
 eapply EQ_TRANS.
 eapply EQ_CONG_FUN_E.
 eauto.
 eauto.
 eapply EQ_REFL.
-eapply RelTerm_implies_WtTm.
 eauto.
 
 eapply EQ_TRANS.
 eauto.
 eauto.
 
-eapply CONV.
-eapply HYP.
-eapply EXT.
-eauto.
-eapply RelType_implies_WfTp.
-eapply RelTerm_implies_RelType.
-eauto.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-eauto.
-eapply RelTerm_implies_WtTm.
-eauto.
-
+auto.
+
+eauto.
+
+
+eauto.
 
 eapply EQ_TRANS.
 eapply EQ_SBSEQ.
 eapply SEXT.
 eauto.
 
-
 eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
 eapply RelTerm_implies_RelType.
 eauto.
 
-eapply CONV.
-eapply RelTerm_implies_WtTm.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SBID.
-
-eapply RelType_implies_WfTp.
-eapply RelTerm_implies_RelType.
-eauto.
+auto.
+
 
 eapply SEXT.
 eapply SSEQ.
 eauto.
 eauto.
 
-eapply CONV.
-eapply HYP.
-eapply EXT.
-eauto.
-eapply RelType_implies_WfTp.
-eapply RelTerm_implies_RelType.
-eauto.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-eauto.
+auto. (*HZZ2*)
+auto.
 
 eapply EQ_CONV.
 eapply EQ_CONG_SB.
 
+unfold Ssing.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eapply SEXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+auto.
+  
+eapply EQ_SB_CONG_SEXT.
+auto.
+eauto.
+
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBID.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+eapply EQ_TP_SYM.
+
+eapply EQ_TP_CONG_SB.
+eauto.
+eauto.
+eauto.
+
+unfold Ssing.
+auto.
+unfold Ssing.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+
+eapply SEXT.
+eauto.
+eauto.
+auto.
+eauto.
+
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+
 
 Qed.