- advances in the theory of cofrees

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma
index bb55c859fb7aa3239d8d2f3123c9ef1aca4bc5d1..3c90f5a9ffc91869a5776ce9a7bfa72a8b9ebf95 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma
@@ -19,7 +19,7 @@ include "basic_2/substitution/lleq.ma".
 (* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
 
 inductive fleq (d) (G) (L1) (T): relation3 genv lenv term ≝
-| fleq_intro: â\88\80L2. L1 â\8b\95[T, d] L2 → fleq d G L1 T G L2 T
+| fleq_intro: â\88\80L2. L1 â\89¡[T, d] L2 → fleq d G L1 T G L2 T
 .
 
 interpretation
@@ -37,7 +37,7 @@ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma fleq_inv_gen: â\88\80G1,G2,L1,L2,T1,T2,d. â¦\83G1, L1, T1â¦\84 â\8b\95[d] ⦃G2, L2, T2⦄ →
-                    â\88§â\88§ G1 = G2 & L1 â\8b\95[T1, d] L2 & T1 = T2.
+lemma fleq_inv_gen: â\88\80G1,G2,L1,L2,T1,T2,d. â¦\83G1, L1, T1â¦\84 â\89¡[d] ⦃G2, L2, T2⦄ →
+                    â\88§â\88§ G1 = G2 & L1 â\89¡[T1, d] L2 & T1 = T2.
 #G1 #G2 #L1 #L2 #T1 #T2 #d * -G2 -L2 -T2 /2 width=1 by and3_intro/
 qed-.