X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffpbs_ext.ma;h=8ae11770f86378858d1bf517d34ad7265ed00fe3;hb=a76f56fdad6348b167376093920650379c9936d4;hp=51575386001fcffcddee26ee0eb8b1311179ebc8;hpb=f7994db705d6c1200cc3e9f1827b7d9f6d0ad001;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
index 515753860..8ae11770f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
@@ -23,9 +23,9 @@ lemma fpbs_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g]
                            ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_fpbsa … H) -H
 #L0 #T0 #HT10 #H10 #HL02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU2 ]
-[ #H destruct lapply (lpxs_cpxs_trans … HTU2 … HL02) -HTU2
-  #HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -T2
-  /3 width=6 by fqus_lpxs_fpbs, ex3_intro/
-| /4 width=6 by fpbs_cpxs_trans, fqus_lpxs_fpbs, ex3_intro/
+[ #H destruct lapply (llpxs_cpxs_trans … HTU2 … HL02)
+  #H elim (fqus_cpxs_trans_neq … H10 … H HnTU2) -H10 -H -HnTU2
+  /4 width=8 by fqus_llpxs_fpbs, llpxs_cpxs_conf_dx, ex3_intro/
+| /4 width=6 by fpbs_cpxs_trans, fqus_llpxs_fpbs, ex3_intro/
 ]
 qed-.