X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Fdefs.ma;h=d9ba6092c50f190f1cd9b62c3155426b74541ed4;hb=c6305166703a17801bbd08a85fe93ef4abf8ff85;hp=90149df3299fce44df34521efdb18f791f55f34c;hpb=049d55c73d1746e15a40e89b17fd88b62f002d93;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 90149df32..d9ba6092c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
@@ -20,7 +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 
-\Rightarrow True | (TCons t ts0) \Rightarrow (let TMP_1 \def (sn3 c t) in 
-(let TMP_2 \def (sns3 c ts0) in (land TMP_1 TMP_2)))].
+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))].