X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_prototerm_lift.ma;h=251d7ba72199c9bfcd93615c9edd395a6da63572;hp=5b18cfb17b9c18f8d66d695b7443c39dcaee62e9;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

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 5b18cfb17..251d7ba72 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
@@ -23,7 +23,7 @@ include "delayed_updating/unwind/unwind2_prototerm.ma".
 (* Constructions with lift_prototerm ****************************************)
 
 lemma lift_unwind2_term_after (f1) (f2) (t):
-      ↑[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
+      🠡[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
 #f1 #f2 #t @subset_eq_trans
 [| @subset_inclusion_ext_f1_compose ]
 @subset_equivalence_ext_f1_exteq #p
@@ -31,7 +31,7 @@ lemma lift_unwind2_term_after (f1) (f2) (t):
 qed.
 
 lemma unwind2_lift_term_after (f1) (f2) (t):
-      ▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t.
+      ▼[f2]🠡[f1]t ⇔ ▼[f2∘f1]t.
 #f1 #f2 #t @subset_eq_trans
 [| @subset_inclusion_ext_f1_compose ]
 @subset_equivalence_ext_f1_exteq #p