Commits

Paweł Wieczorek  committed 2cc1b25

The _App case finished

  • Participants
  • Parent commits c5c09ae
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

 eauto.
 eauto.
 
+assert ( Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HZZZ0.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmSb A SB) as HZZZ1.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+
+
 assert (Delta0 |-- [Sseq (Sseq SB Sup) (Sext (Sups i) a)] === [Sseq SB (Sups i)] : Gamma ) as HZZ1.
 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.
-
-
+eauto.
+eauto.
+eauto.
+eauto.
+
+(**)
 eapply EQ_SB_CONG_SEXT.
 apply HZZ1.
 eauto.
+(**)
+
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ2.
 
 eapply EQ_CONV.
 eapply EQ_SBVAR.
 eauto.
 eapply RelTerm_implies_WtTm.
 eauto.
-
 eapply EQ_TP_TRANS.
 eapply EQ_TP_SBSEQ.
 eauto.
 apply HZZ1.
 eauto.
 eauto.
-
-
+eauto.
 
 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 SB) (Sups i)) as HZZZ0.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmSb A SB) as HZZZ1.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+
 assert (Delta0 |-- a : TmSb (TmSb A (Sseq SB (Sups i))) Sid) as HZZ1.
 eapply CONV.
 eapply RelTerm_implies_WtTm.
 eauto. 
 
 
+
 assert ( Delta0,, TmSb A (Sseq SB (Sups i)) |-- TmVar
    : TmSb A (Sseq (Sseq SB (Sups i)) Sup)) as HZZ2.
 
 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_SUP.
 eauto.
 eauto.
-eapply RelTerm_implies_WtTm.
-eauto.
-eauto.
-
+eauto.
+eauto.
+
+assert (Delta0 |--  [Sext Sid a]: Delta0,, TmSb A (Sseq SB (Sups i))) as HZZZ4.
+eapply SEXT.
+eauto.
+eauto.
+auto.
 
 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.
 eauto.
 
 eapply EQ_SB_REFL.
 eauto.
 
+(*
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ2.
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+apply HZZ1.
+eauto.
+eauto.
+*)
+
+
 
 assert (
   Delta0
 ) as HZZ6.
 eapply EQ_TP_SYM.
 eapply EQ_TP_SBSEQ.
+eauto.
 eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+auto.
+eauto.
+
+
+assert (Delta,, TmSb A SB |-- TmVar : TmSb A (Sseq SB Sup)) as HZZ7.
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+
+assert(Delta0 |-- TmSb TmVar (Sext Sid a) === a :TmSb (TmSb A (Sseq SB (Sups i))) Sid) as HZZZ5.
+eapply EQ_SBVAR.
 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.
+assert ( Delta0 |-- TmSb TmVar (Sext Sid a) === a
+   : TmSb A (Sseq (Sseq (Sseq SB (Sups i)) Sup) (Sext Sid a))) as HZZZ6.
+
+eapply EQ_CONV.
+eauto.
+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.
+
 (**)
 
 eapply EQ_CONV.
 eapply EQ_TRANS.
 eapply EQ_SBSEQ.
 unfold Ssing.
-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.
-
+eauto.
+eauto.
 auto. (*HZZ2*)
 auto.
 
 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.
+eauto.
 
 eapply SEXT.
 eapply SSEQ.
 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.
 
 
 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.
-
+eauto.
 eapply SEXT.
 eauto.
 eauto.
 eapply EQ_TP_SYM.
 eapply EQ_TP_TRANS.
 eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eauto.
+eauto.
+
+
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ7.
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eauto.
+
+eapply EQ_SB_SYM.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
 eapply SEXT.
 eauto.
 eauto.
-eapply RelTerm_implies_WtTm.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_CONG_SB.
-
+auto.
+
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_TRANS.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ7.
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eauto.
+eauto.
+
+(***)
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eauto.
 
 Qed.