X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffpbs_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffpbs_lift.ma;h=4895dccf546b7f55a84c7f812abbabe3fc9e4964;hb=890a19d326338d96879dedce1eadc7c91a3beac2;hp=8bcc50cd1dced07baaa5b4546e6d20cd3f4fc066;hpb=0f34e7f3ada66fdc9044b5ed5c5f59ea36d3c6a2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
index 8bcc50cd1..4895dccf5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/reduction/fpb_lift.ma".
 include "basic_2/computation/cpxs_lift.ma".
 include "basic_2/computation/fpbs.ma".
 
@@ -23,8 +24,7 @@ lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
                    ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
 /3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed.
 
-(* Note: this should be moved *)
 lemma ssta_fpbs: ∀h,g,G,L,T,U,l.
                  ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
                  ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
-/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed.
+/4 width=2 by fpb_fpbs, ssta_fpb/ qed.