X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fprototerm_constructors_eq.ma;h=c99cb57750548485fc02b19954e1fd900362835d;hp=4a83b790efe57b98d423129c50c1aab43d28e71e;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hpb=48cd63fc7f4415925582eae224a36a9c1bb3cc06

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
index 4a83b790e..c99cb5775 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
@@ -23,3 +23,42 @@ lemma iref_eq_repl (t1) (t2) (k):
       t1 ⇔ t2 → 𝛕k.t1 ⇔ 𝛕k.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.
+
+lemma abst_eq_repl (t1) (t2):
+      t1 ⇔ t2 → 𝛌.t1 ⇔ 𝛌.t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
+
+lemma appl_eq_repl (u1) (u2) (t1) (t2):
+      u1 ⇔ u2 → t1 ⇔ t2 → ＠u1.t1 ⇔ ＠u2.t2.
+/2 width=1 by subset_equivalence_ext_f1_1_bi/
+qed.
+
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_abst_hd (t) (p):
+      t⋔p ⇔ (𝛌.t)⋔(𝗟◗p).
+#t #p @conj #r #Hr
+[ /2 width=3 by ex2_intro/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=1 by in_comp_inv_abst_hd/
+]
+qed.
+
+lemma grafted_appl_sd (v) (t) (p):
+      v⋔p ⇔ (＠v.t)⋔(𝗦◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_introl/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=2 by in_comp_inv_appl_sd/
+]
+qed.
+
+lemma grafted_appl_hd (v) (t) (p):
+      t⋔p ⇔ (＠v.t)⋔(𝗔◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_intror/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=2 by in_comp_inv_appl_hd/
+]
+qed.