update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / prototerm_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
index 5604578e52fa9839edb1a6ae9c6caf44344f5ebe..bf73d3005dfc27f1dcf99d50eff17050225e4f21 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
@@ -24,6 +24,18 @@ lemma grafted_empty_dx (t):
 /2 width=1 by conj/
 qed.
 
+lemma grafted_incl_repl (t1) (t2) (p):
+      t1 ⊆ t2 → t1⋔p ⊆ t2⋔p.
+#t1 #t2 #p #Ht #q #Hq
+/2 width=1 by/
+qed.
+
+lemma grafted_eq_repl (t1) (t2) (p):
+      t1 ⇔ t2 → t1⋔p ⇔ t2⋔p.
+#t1 #t2 #p * #H1t #H2t
+/3 width=1 by conj, grafted_incl_repl/
+qed.
+
 (* Constructions with prototerm_root ****************************************)
 
 lemma prototerm_root_incl_repl: