X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_prototerm_constructors.ma;h=6e3c96fe7fbd40e6fe6d359e40e1815f503e24e8;hb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a;hp=96fc1d02ef12caf364103ee94bf14cffba06f2e3;hpb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
index 96fc1d02e..6e3c96fe7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
@@ -20,21 +20,43 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 
 (* Constructions with constructors for prototerm ****************************)
 
-lemma unwind2_term_iref_sn (f) (t) (k:pnat):
-      ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
-#f #t #k #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱k◗𝗺◗q))
-/2 width=1 by in_comp_iref_hd/
-qed-.
-
-lemma unwind2_term_iref_dx (f) (t) (k:pnat):
-      ▼[f](𝛕k.t) ⊆ ▼[f∘𝐮❨k❩]t.
-#f #t #k #p * #q #Hq #H0 destruct
-elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
+lemma unwind2_term_oref_pap (f) (k):
+      (⧣(f＠⧣❨k❩)) ⇔ ▼[f]⧣k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_unwind2_path_term/
+| #q * #H0 destruct //
+]
+qed.
 
 lemma unwind2_term_iref (f) (t) (k:pnat):
       ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
-/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
+#f #t #k @conj
+#p * #q #Hq #H0 destruct
+[ @(ex2_intro … (𝗱k◗𝗺◗q))
+  /2 width=1 by in_comp_iref_hd/
+| elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
+  /2 width=1 by in_comp_unwind2_path_term/
+]
+qed.
+
+lemma unwind2_term_abst (f) (t):
+      (𝛌.▼[⫯f]t) ⇔ ▼[f]𝛌.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma unwind2_term_appl (f) (v) (t):
+      ＠▼[f]v.▼[f]t ⇔ ▼[f]＠v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
 qed.