Commits

Paweł Wieczorek  committed 01a8d1c

The Rel_Fundamental_App is prooved.

  • Participants
  • Parent commits 78ccbfa
  • Branches weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

 eauto.
 eauto.
 
-
-
-(*--------------------------------------*)
-
-
-assert (Delta |-- TmSb (TmSb B (Ssing N)) SB === TmSb XF (Sext Sid (TmSb N SB))) as HXX5.
-
-admit.
-admit.
-(**)
-
-
-
+assert (Gamma,,A |-- B) as HXX9.
+assert (Gamma |-- TmFun A B) as HYY1 by eauto.
+clear_inversion HYY1.
+auto.
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SYM.
+eapply HXX8.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+unfold Ssing.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_SIDL.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply CONV.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDR.
+eauto.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDL.
+eauto.
+eapply EQ_TP_REFL.
+eauto.
+
+eapply EQ_SB_REFL.
+eauto.
+
+eapply EQ_TP_REFL.
+eauto.
+
+eauto.
+
+eapply EQ_CONG_FUN_E.
+eapply EQ_SBID.
+eauto.
+
+eapply EQ_REFL.
+eauto.
 Qed.