update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_prototerm_eq.ma

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 d23c7f058de4ebdcb26b6b2b3d3cb030485e586c..70d41140bd2d28c7c71b5cd993b5a8c4ea2e42b0 100644 (file)
--- 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.