X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Fdefs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Fdefs.ma;h=c6980318bca9e430dd7c9f1cd6d310930d2246c4;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=90149df3299fce44df34521efdb18f791f55f34c;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;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..c6980318b 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
@@ -21,6 +21,5 @@ inductive sn3 (c: C): T \to Prop \def
 (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)))].
+\Rightarrow True | (TCons t ts0) \Rightarrow (land (sn3 c t) (sns3 c ts0))].