- advances in the theory of cofrees

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lleq_lleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index a3a276ff367e31236fb25bd784f58d40ab966ea4..abee448a3bc70740bb8cf207e1bc4a47044a828b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -19,14 +19,14 @@ include "basic_2/substitution/lleq_ldrop.ma".
 theorem lleq_trans: ∀d,T. Transitive … (lleq d T).
 /2 width=3 by lleq_llpx_sn_trans/ qed-.
 
-theorem lleq_canc_sn: â\88\80L,L1,L2,T,d. L â\8b\95[d, T] L1â\86\92 L â\8b\95[d, T] L2 â\86\92 L1 â\8b\95[d, T] L2.
+theorem lleq_canc_sn: â\88\80L,L1,L2,T,d. L â\89¡[d, T] L1â\86\92 L â\89¡[d, T] L2 â\86\92 L1 â\89¡[d, T] L2.
 /3 width=3 by lleq_trans, lleq_sym/ qed-.
 
-theorem lleq_canc_dx: â\88\80L1,L2,L,T,d. L1 â\8b\95[d, T] L â\86\92 L2 â\8b\95[d, T] L â\86\92 L1 â\8b\95[d, T] L2.
+theorem lleq_canc_dx: â\88\80L1,L2,L,T,d. L1 â\89¡[d, T] L â\86\92 L2 â\89¡[d, T] L â\86\92 L1 â\89¡[d, T] L2.
 /3 width=3 by lleq_trans, lleq_sym/ qed-.
 
-(* Note: lleq_nlleq_trans: â\88\80d,T,L1,L. L1â\8b\95[T, d] L →
-                           â\88\80L2. (L â\8b\95[T, d] L2 â\86\92 â\8a¥) â\86\92 (L1 â\8b\95[T, d] L2 → ⊥).
+(* Note: lleq_nlleq_trans: â\88\80d,T,L1,L. L1â\89¡[T, d] L →
+                           â\88\80L2. (L â\89¡[T, d] L2 â\86\92 â\8a¥) â\86\92 (L1 â\89¡[T, d] L2 → ⊥).
 /3 width=3 by lleq_canc_sn/ qed-.
 works with /4 width=8/ so lleq_canc_sn is more convenient
 *)