X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_prototerm_eq.ma;h=70d41140bd2d28c7c71b5cd993b5a8c4ea2e42b0;hp=d23c7f058de4ebdcb26b6b2b3d3cb030485e586c;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
index d23c7f058..70d41140b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
@@ -22,23 +22,23 @@ include "delayed_updating/substitution/lift_prototerm.ma".
 (* Constructions with subset_equivalence ************************************)
 
 lemma lift_term_eq_repl_sn (f1) (f2) (t):
-      f1 ≗ f2 → ↑[f1]t ⇔ ↑[f2]t.
+      f1 ≗ f2 → 🠡[f1]t ⇔ 🠡[f2]t.
 /3 width=1 by subset_equivalence_ext_f1_exteq, lift_path_eq_repl/
 qed.
 
 lemma lift_term_eq_repl_dx (f) (t1) (t2):
-      t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2.
+      t1 ⇔ t2 → 🠡[f]t1 ⇔ 🠡[f]t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.
 
 lemma lift_term_grafted_sn (f) (t) (p):
-      ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(↑[f]p).
+      🠡[🠢[f]p](t⋔p) ⊆ (🠡[f]t)⋔(🠡[f]p).
 #f #t #p #q * #r #Hr #H0 destruct
 /2 width=3 by ex2_intro/
 qed-.
 
 lemma lift_term_grafted_dx (f) (t) (p):
-      (↑[f]t)⋔(↑[f]p) ⊆ ↑[↑[p]f](t⋔p).
+      (🠡[f]t)⋔(🠡[f]p) ⊆ 🠡[🠢[f]p](t⋔p).
 #f #t #p #q * #r #Hr #H0
 elim (lift_path_inv_append_sn … (sym_eq … H0)) -H0
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
@@ -47,9 +47,9 @@ lapply (lift_path_inj … Hp0) -Hp0 #Hp0 destruct
 qed-.
 
 lemma lift_term_grafted (f) (t) (p):
-      ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(↑[f]p).
+      🠡[🠢[f]p](t⋔p) ⇔ (🠡[f]t)⋔(🠡[f]p).
 /3 width=1 by lift_term_grafted_sn, lift_term_grafted_dx, conj/ qed.
 
 lemma lift_term_grafted_S (f) (t) (p):
-      ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((↑[f]p)◖𝗦).
+      🠡[🠢[f]p](t⋔(p◖𝗦)) ⇔ (🠡[f]t)⋔((🠡[f]p)◖𝗦).
 // qed.