X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_prototerm_lift.ma;h=8d987dfb7759ae0338f9d050b5769a1ac89d740f;hb=3af42b8f2cb1956eed14edcc0adb9df92601f248;hp=8e3d2cf2f74d4c57c396a22c4c16adc2763f4097;hpb=97ff918432e878ab8314c72fe2b948a253b26e21;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
index 8e3d2cf2f..8d987dfb7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
@@ -22,10 +22,18 @@ include "delayed_updating/unwind/unwind2_prototerm.ma".
 
 (* Constructions with lift_prototerm ****************************************)
 
-lemma unwind2_lift_term_after (f1) (f2) (t):
+lemma lift_unwind2_term_after (f1) (f2) (t):
       ↑[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
 #f1 #f2 #t @subset_eq_trans
 [| @subset_inclusion_ext_f1_compose ]
 @subset_equivalence_ext_f1_exteq #p
-@unwind2_lift_path_after
+@lift_unwind2_path_after
+qed.
+
+lemma unwind2_term_after_lift (f1) (f2) (t):
+      ▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[| @subset_inclusion_ext_f1_compose ]
+@subset_equivalence_ext_f1_exteq #p
+@unwind2_path_after_lift
 qed.