minor web site update

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / leq_leq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
index d07a5f2e6b977adb4dbf42b47279b212d8276faa..6c0059a6f1ff4da663701dfedcdf738e5ff3205d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
@@ -32,14 +32,14 @@ theorem leq_trans: ∀d,e. Transitive … (leq d e).
 ]
 qed-.
 
-theorem leq_canc_sn: â\88\80d,e,L,L1,L2. L â\89\83[d, e] L1 â\86\92 L â\89\83[d, e] L2 â\86\92 L1 â\89\83[d, e] L2.
+theorem leq_canc_sn: â\88\80d,e,L,L1,L2. L ⩬[d, e] L1 â\86\92 L ⩬[d, e] L2 â\86\92 L1 ⩬[d, e] L2.
 /3 width=3 by leq_trans, leq_sym/ qed-.
 
-theorem leq_canc_dx: â\88\80d,e,L,L1,L2. L1 â\89\83[d, e] L â\86\92 L2 â\89\83[d, e] L â\86\92 L1 â\89\83[d, e] L2.
+theorem leq_canc_dx: â\88\80d,e,L,L1,L2. L1 ⩬[d, e] L â\86\92 L2 ⩬[d, e] L â\86\92 L1 ⩬[d, e] L2.
 /3 width=3 by leq_trans, leq_sym/ qed-.
 
-theorem leq_join: â\88\80L1,L2,d,i. L1 â\89\83[d, i] L2 →
-                  â\88\80e. L1 â\89\83[i+d, e] L2 â\86\92 L1 â\89\83[d, i+e] L2.
+theorem leq_join: â\88\80L1,L2,d,i. L1 ⩬[d, i] L2 →
+                  â\88\80e. L1 ⩬[i+d, e] L2 â\86\92 L1 ⩬[d, i+e] L2.
 #L1 #L2 #d #i #H elim H -L1 -L2 -d -i //
 [ #I #L1 #L2 #V #e #_ #IHL12 #e #H
   lapply (leq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by leq_pair/