- some refactoring and minor additions

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
index a08672bc8284972392197e2b00d7943ac312cbb6..6a9cf9d45c0e1b0a680ba5e210be9ccaf56e536c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
@@ -12,22 +12,24 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lleq_fqus.ma".
-include "basic_2/substitution/lleq_lleq.ma".
-include "basic_2/computation/llpxs_lleq.ma".
+include "basic_2/multiple/lleq_fqus.ma".
+include "basic_2/multiple/lleq_lleq.ma".
+include "basic_2/computation/cpxs_lleq.ma".
+include "basic_2/computation/lpxs_lleq.ma".
 include "basic_2/computation/fpbu.ma".
 
 (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
 
 (* Properties on lazy equivalence for local environments ********************)
 
-lemma lleq_fpbu_trans: â\88\80h,g,F,K1,K2,T. K1 â\8b\95[T, 0] K2 →
+lemma lleq_fpbu_trans: â\88\80h,g,F,K1,K2,T. K1 â\89¡[T, 0] K2 →
                        ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ →
-                       â\88\83â\88\83L1. â¦\83F, K1, Tâ¦\84 â\89»[h, g] â¦\83G, L1, Uâ¦\84 & L1 â\8b\95[U, 0] L2.
+                       â\88\83â\88\83L1. â¦\83F, K1, Tâ¦\84 â\89»[h, g] â¦\83G, L1, Uâ¦\84 & L1 â\89¡[U, 0] L2.
 #h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
 [ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2
   /3 width=3 by fpbu_fqup, ex2_intro/
-| /4 width=10 by fpbu_cpxs, lleq_cpxs_conf_sn, lleq_cpxs_trans, ex2_intro/
-| /5 width=3 by fpbu_llpxs, lleq_llpxs_trans, lleq_canc_sn, ex2_intro/
+| /4 width=10 by fpbu_cpxs, cpxs_lleq_conf_sn, lleq_cpxs_trans, ex2_intro/
+| #L2 #HKL2 #HnKL2 elim (lleq_lpxs_trans … HKL2 … HT) -HKL2
+  /6 width=3 by fpbu_lpxs, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *)
 ]
 qed-.