X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Fdefs.ma;h=d9ba6092c50f190f1cd9b62c3155426b74541ed4;hb=ab2f735d97d2b9c965f13527d5f6f61048d29b22;hp=c6980318bca9e430dd7c9f1cd6d310930d2246c4;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
index c6980318b..d9ba6092c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
@@ -20,6 +20,6 @@ inductive sn3 (c: C): T \to Prop \def
 | sn3_sing: \forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall 
 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)).
 
-let rec sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
+rec definition sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
 \Rightarrow True | (TCons t ts0) \Rightarrow (land (sn3 c t) (sns3 c ts0))].