X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsn3%2Fdefs.ma;h=90149df3299fce44df34521efdb18f791f55f34c;hb=049d55c73d1746e15a40e89b17fd88b62f002d93;hp=686e6c673f51fabd8323f65712f1057bc24bc4e0;hpb=f7b122ac0979ee71c222d09d3ce32ded37767cd5;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 686e6c673..90149df32 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
@@ -14,16 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pr3/defs.ma".
+include "basic_1/pr3/defs.ma".
 
 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)).
 
-definition sns3:
- C \to (TList \to Prop)
-\def
- let rec 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))]) 
-in sns3.
+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)))].