update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_prototerm_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
index 920a16cf0d2cc59a0c983c6f98cfbbade6406e6f..0b3ba39b001f5f7e1787537fb1cafa0c0ad1c200 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
@@ -38,3 +38,20 @@ lemma lift_term_after (f1) (f2) (t):
 | @subset_equivalence_ext_f1_exteq /2 width=5/
 ]
 qed.
+
+lemma lift_term_id_sn (t):
+      t ⊆ ↑[𝐢]t.
+#t #p #Hp
+>(lift_path_id p)
+/2 width=1 by in_comp_lift_bi/
+qed-.
+
+lemma lift_term_id_dx (t):
+      ↑[𝐢]t ⊆ t.
+#t #p * #q #Hq #H destruct //
+qed-.
+
+lemma lift_term_id (t):
+      t ⇔ ↑[𝐢]t.
+/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/
+qed.