update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_prototerm_lift.ma

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 8e3d2cf2f74d4c57c396a22c4c16adc2763f4097..251d7ba72199c9bfcd93615c9edd395a6da63572 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
@@ -18,12 +18,20 @@ include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/unwind/unwind2_path_lift.ma".
 include "delayed_updating/unwind/unwind2_prototerm.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 (* Constructions with lift_prototerm ****************************************)
 
+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
+@lift_unwind2_path_after
+qed.
+
 lemma unwind2_lift_term_after (f1) (f2) (t):
-      â\86\91[f2]â\96¼[f1]t ⇔ ▼[f2∘f1]t.
+      â\96¼[f2]ð\9f ¡[f1]t ⇔ ▼[f2∘f1]t.
 #f1 #f2 #t @subset_eq_trans
 [| @subset_inclusion_ext_f1_compose ]
 @subset_equivalence_ext_f1_exteq #p