X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffpbs_alt.ma;h=cc6ae13627effee4aef12f62e67dd92d14bfc788;hb=4b8544042a6f3c5f5d303d4120c69abbc34ce15b;hp=047fd164a8fbe2642399b930d5b8a5a8a81b171e;hpb=7a25b8fcba2436a75556db1725c6e1be78a9faca;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
index 047fd164a..cc6ae1362 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
@@ -13,13 +13,12 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstaralt_8.ma".
-include "basic_2/substitution/lleq_fqus.ma".
-include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/multiple/lleq_fqus.ma".
 include "basic_2/computation/cpxs_lleq.ma".
 include "basic_2/computation/lpxs_lleq.ma".
 include "basic_2/computation/fpbs.ma".
 
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+(* "QREST" PARALLEL COMPUTATION FOR CLOSURES ********************************)
 
 (* Note: alternative definition of fpbs *)
 definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝
@@ -64,7 +63,7 @@ qed.
 theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
                         ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 *
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpb_lleq/
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_lleq/
 qed-.
 
 (* Advanced properties ******************************************************)