X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffsb_aaa.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffsb_aaa.ma;h=b95c6ced6f27940cee4ca3a022484537d759e059;hb=cacd7323994f7621286dbfd93bbf4c50acfbe918;hp=7ea1776a0299a280012d08896c80c91b004eda6c;hpb=f76594123e375bd7852c9421fe260a7bec693a92;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
index 7ea1776a0..b95c6ced6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
@@ -21,7 +21,6 @@ include "basic_2/rt_computation/fsb_csx.ma".
 
 (* Main properties with atomic arity assignment for terms *******************)
 
-(* Note: this is the "big tree" theorem *)
 theorem aaa_fsb: ∀h,G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ≥[h] 𝐒⦃G,L,T⦄.
 /3 width=2 by aaa_csx, csx_fsb/ qed.