X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_coafter.ma;h=f93a968b0f3a373adbe8947ee0db8df00ebc7306;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=7758003287dde4ed294fe85588d6a93d4b589aa9;hpb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;p=helm.git

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 775800328..f93a968b0 100644
--- 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.