commit of the "computation" component with lazy pointwise extensions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpbs_ext.ma

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 51575386001fcffcddee26ee0eb8b1311179ebc8..8ae11770f86378858d1bf517d34ad7265ed00fe3 100644 (file)
--- 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-.