X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fprototerm_proper_inner.ma;h=9f09200d3708fa7f75b0a49b6e137d1811f37907;hb=e4328f6887dc0235d49d965a5ba44787b1754b80;hp=e3665476b9e10e1fc08f397eb34a9b9268459f44;hpb=23e56dd2f1ff99613b69e1ed2a9f26e752304290;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
index e3665476b..9f09200d3 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
@@ -18,7 +18,7 @@ include "ground/lib/subset_overlap.ma".
 
 (* PROPER CONDITION FOR PROTOTERM *******************************************)
 
-(* Constructions with inner condition for prototerm *************************)
+(* Constructions with pic ***************************************************)
 
 lemma term_proper_outer (t):
       t ⧸≬ 𝐈 → t ϵ 𝐏.