milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_coafter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index 7758003287dde4ed294fe85588d6a93d4b589aa9..f93a968b0f3a373adbe8947ee0db8df00ebc7306 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -44,7 +44,7 @@ interpretation "functional co-composition (nstream)"
 
 (* Basic properties on funs *************************************************)
 
-(* Note: we need theese since matita blocks recursive δ when ι is blocked *)  
+(* Note: we need theese since matita blocks recursive δ when ι is blocked *)
 lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2).
 * #n2 #f2 * //
 qed.