X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flpxs_cpxs.ma;h=10600383a97ccc1a1257208cbb2bf8ffc5127552;hb=b5d702735754632652b2659c425dd67d7f92f24b;hp=2d197c95b2dabcc619574d1106314419d5cf50e2;hpb=7ad8c044ab33ea0f2aebb1c40fa20340d7f2f3eb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
index 2d197c95b..10600383a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -107,7 +107,7 @@ lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
 #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
 #L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT0 … HT3) -T
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
 /3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
 qed-.