notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lifts_lift_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
index 559e62659ec9db7ed63134ffc03ef4de91f3e517..ecba0fd777862290a907a0b34c32a241d39b58a4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
@@ -21,9 +21,9 @@ include "basic_2/multiple/lifts_vector.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: lifts1_xhg (right to left) *)
-lemma liftsv_liftv_trans_le: â\88\80T1s,Ts,des. â\87§*[des] T1s ≡ Ts →
-                             â\88\80T2s:list term. â\87§[0, 1] Ts ≡ T2s →
-                             â\88\83â\88\83T0s. â\87§[0, 1] T1s â\89¡ T0s & â\87§*[des + 1] T0s ≡ T2s.
+lemma liftsv_liftv_trans_le: â\88\80T1s,Ts,des. â¬\86*[des] T1s ≡ Ts →
+                             â\88\80T2s:list term. â¬\86[0, 1] Ts ≡ T2s →
+                             â\88\83â\88\83T0s. â¬\86[0, 1] T1s â\89¡ T0s & â¬\86*[des + 1] T0s ≡ T2s.
 #T1s #Ts #des #H elim H -T1s -Ts
 [ #T1s #H
   >(liftv_inv_nil1 … H) -T1s /2 width=3/