X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs.ma;h=74eae9335e51fd82f0e20a12add8b9ecfb0a8779;hb=afd4afa9489fa65019ad7cdc274e261f6993b871;hp=2b13efb0e361d321039ece7f0179b4f6ac2fa61f;hpb=dd74d1964ef07de249385a48f28302b427c0d287;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
index 2b13efb0e..74eae9335 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
@@ -53,7 +53,7 @@ lemma fpbs_strap2: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, o] 
                    ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
 /2 width=5 by tri_TC_strap/ qed-.
 
-(* Basic_2A1: uses: lleq_fpbs *)
+(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *)
 lemma ffdeq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
 /3 width=1 by fpbq_fpbs, fpbq_ffdeq/ qed.