]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight_bind.ma
update in basic_2 and ground_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lifts_weight_bind.ma
index 152ecbba1223effb60e5d6f2515cd790bb8d124c..f151431172826d6aa62323d65235179ade7d81cb 100644 (file)
@@ -20,6 +20,6 @@ include "basic_2/relocation/lifts_bind.ma".
 
 (* Forward lemmas with weight for binders ***********************************)
 
-lemma liftsb_fwd_bw: â\88\80f,I1,I2. â¬\86*[f] I1 â\89¡ I2 → ♯{I1} = ♯{I2}.
+lemma liftsb_fwd_bw: â\88\80f,I1,I2. â¬\86*[f] I1 â\89\98 I2 → ♯{I1} = ♯{I2}.
 #f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/
 qed-.