Commits

Paweł Wieczorek committed c82049b

added simple helper

Comments (0)

Files changed (1)

Nbe/Model/LogRelTm.v

 eauto.
 Qed.
 
+Corollary RelTerm_ClosedUnderPer'': forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  forall t dt DT'' (HDT' : DT' === DT'' #in# PerType),
+   Gamma ||- t : T #aeq# dt #in# HDT ->
+   Gamma ||- t : T #aeq# dt #in# HDT'
+.
+Proof.
+intros.
+
+destruct ClosedUnderPer with (Gamma := Gamma) (T := T) (DT := DT) (DT' := DT') (HDT := HDT) (DT'' := DT'') (HDT' := HDT'); auto.
+eapply RelTerm_implies_RelType.
+apply H.
+
+assert (exists PT, Interp DT PT) as HX1.
+eapply RelTerm_has_Interp.
+eauto.
+
+destruct HX1 as [PT HPT].
+
+assert (dt === dt #in# PT) as HX2.
+eapply RelTerm_resp_Interp.
+eauto.
+auto.
+
+eapply H1.
+eauto.
+eauto.
+auto.
+Qed.
+
 
 Lemma RelType_ClosedUnderPer_sym: forall Delta T DT DT'
   (HDT1 : DT === DT' #in# PerType) (HDT2: DT' === DT #in# PerType),