still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fsb_aaa.ma

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 7ea1776a0299a280012d08896c80c91b004eda6c..b95c6ced6f27940cee4ca3a022484537d759e059 100644 (file)
--- 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.