more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_fqus.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
index 03ae7cc3797aa2fc3bbd0c1b67014159bbb28141..acef276fa2851d4a9691671a0e068afa62c45fae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/csx_lsubr.ma".
 
 (* Properties with extended supclosure **************************************)
 
-lemma csx_fqu_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90[b] ⦃G2,L2,T2⦄ →
+lemma csx_fqu_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82[b] ⦃G2,L2,T2⦄ →
                     ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [ /3 width=5 by csx_inv_lref_pair, drops_refl/
@@ -31,19 +31,19 @@ lemma csx_fqu_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2
 ]
 qed-.
 
-lemma csx_fquq_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] ⦃G2,L2,T2⦄ →
+lemma csx_fquq_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82⸮[b] ⦃G2,L2,T2⦄ →
                      ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
 #h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
 * #HG #HL #HT destruct //
 qed-.
 
-lemma csx_fqup_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90+[b] ⦃G2,L2,T2⦄ →
+lemma csx_fqup_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82+[b] ⦃G2,L2,T2⦄ →
                      ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
 /3 width=6 by csx_fqu_conf/
 qed-.
 
-lemma csx_fqus_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma csx_fqus_conf: â\88\80h,b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                      ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
 /3 width=6 by csx_fquq_conf/