Commits

Paweł Wieczorek committed 813f3c6

less admits!

Comments (0)

Files changed (1)

Nbe/Model/LogRelSb.v

 apply RelSb_lift1; auto.
 (**)
 
+assert (Gamma |= A) as HvalA.
+eapply Valid_for_WfTp.
+eauto.
+
+clear_inversion HvalA.
+assert ([denv] === [denv] #in# Gamma) as Hval.
+eauto.
+
+specialize (H2 _ _ Hval).
+destruct H2 as [DA' [DA'']].
+program_simpl.
+elim_deters.
+clear_dups.
+rename H5 into HDA.
 
 
 (*old*)
 
+assert (Gamma ,, A ||- TmSb A Sup #in# HDA) as HZ1.
+eapply Rel_Fundamental_Tp with (Gamma := Gamma) (T := A) (Delta := (Gamma,,A)) (SB := Sup) (denv := denv); auto.
+
+(**)
+
+assert (exists PA, Interp DA PA) as HPA.
+eauto.
+destruct HPA as [PA HPA].
+
 apply RelSb_ClosedUnderEq with (sb1 := Sext Sup TmVar); auto.
 econstructor 2.
 eapply HSup. 
-
-eapply Rel_Fundamental_Tp with (Gamma := Gamma) (T := A) (Delta := (Gamma,,A)) (SB := Sup) (denv := denv); auto.
-eauto.
-renamer.
-assert (DA_denv0 = DA_denv) by eauto.
-subst. clear_dups.
-
-
-eauto.
-eapply RelSid_Var; eauto.
-
-(*
-eapply Rel_Fundamental_Tp with (Gamma := Gamma) (T := A) (Delta := (Gamma,,A)) (SB := Sup) (denv := denv); auto.
-program_simpl.
-renamer.
-assert (DA_denv0 = DA_denv) by eauto.
-subst. clear_dups.
-
-apply RelSb_ClosedUnderEq with (sb1 := Sext Sup TmVar); auto.
-econstructor 2; eauto.
-eapply RelSid_Var; eauto.
-*)
-admit.
+eauto.
+eapply RelSid_Var.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+
+
+eapply Reflect_Characterization.
+eauto.
+eauto.
+
+eauto.
+
 Qed.
 
 (******************************************************************************