1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed be0f605

almost finished _Abs case in fundamental lemma

  • Participants
  • Parent commits 0d7de0e
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

View file
  • Ignore whitespace
 eauto.
 eauto.
 
-(*
-assert (Delta0 ||- [Sext (Sseq SB (Sups i)) a] : Gamma,,A #aeq# Dext denv da) as HYY5.
+assert (Gamma |-- A) as HYY5.
+assert (Gamma,,A |-- ) by eauto.
+clear_inversion H5.
+auto.
+
+assert (Delta0 |-- TmSb (TmSb A SB) (Sups i) === TmSb A (Sseq SB (Sups i))) as HYY6.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 ||- a : TmSb A (Sseq SB (Sups i)) #aeq# da #in# HDA) as HYY7.
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 ||- [Sext (Sseq SB (Sups i)) a] : Gamma,,A #aeq# Dext denv da) as HYY8.
 econstructor 2.
 eauto.
 eauto.
-
-specialize (H0 Delta0 (Sext (Sseq SB (Sups i)) a) denv).
-*)
-admit.
+eauto.
+eapply EQ_SB_REFL.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply RelSb_valenv.
+eauto.
+eauto.
+eauto.
+eauto.
+
+move H0 at bottom.
+specialize (H0 Delta0 (Sext (Sseq SB (Sups i)) a) (Dext denv da)).
+specialize (H0 HYY8).
+specialize (H0 _ _ (  HAPPDB da da DB DB' PDA_denv0 HPA0 Hda Happ Happ' )).
+specialize (H0 dtm0).
+
+assert (EvalTm B (Dext denv da) DB) as HYY9.
+inversion Happ.
+auto.
+
+specialize (H0 HYY9 Hdtm0).
+
+
 
 
 Qed.