- "small step" version of "big tree" theorem proved

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma
index 73e04e3d587775fad6aa273ddb430eac511346fe..c909e2ed6ff5c25f506fa821ac23217d7d59e06b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma
@@ -35,7 +35,7 @@ lemma bteq_sym: tri_symmetric … bteq.
 #G1 #G2 #L1 #L2 #T1 #T2 * //
 qed-.
 
-lemma bteq_dec: â\88\80G1,G2,L1,L2,T1,T2. Decidable (â¦\83G1, L1, T1â¦\84 ⪴ ⦃G2, L2, T2⦄).
+lemma bteq_dec: â\88\80G1,G2,L1,L2,T1,T2. Decidable (â¦\83G1, L1, T1â¦\84 â\8b\95 ⦃G2, L2, T2⦄).
 #G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2)
 #H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
 elim (eq_nat_dec (|L1|) (|L2|))