X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream.ma;h=c852317f895c60e34fc403dd6f7c2572bc0a3620;hb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;hp=8d7dacc4ed7632a7270f33473076f238b6c20601;hpb=ad3d1cac216cf3882e4adf691b27c00838c6b9b1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index 8d7dacc4e..c852317f8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -25,7 +25,7 @@ interpretation "push (nstream)" 'Lift f = (push f).
 
 definition next: rtmap → rtmap.
 * #n #f @(⫯n@f)
-qed.
+defined.
 
 interpretation "next (nstream)" 'Successor f = (next f).