X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcimp%2Fdefs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcimp%2Fdefs.ma;h=fce9abdd15749acd36f6539a886eced32a703656;hb=d795687ffe924872a5e36122c2bd3069d6409454;hp=b45b64b59d253f4e4da09477c9f7f609e1bbb7ab;hpb=8c62eb7de90e3c9a3a960fb0b3845bc561dddb75;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/cimp/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/cimp/defs.ma
index b45b64b59..fce9abdd1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/cimp/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/cimp/defs.ma
@@ -14,12 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/getl/defs.ma".
+include "basic_1/getl/defs.ma".
 
 definition cimp:
  C \to (C \to Prop)
 \def
  \lambda (c1: C).(\lambda (c2: C).(\forall (b: B).(\forall (d1: C).(\forall 
-(w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to (ex C 
-(\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w)))))))))).
+(w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to (let TMP_3 
+\def (\lambda (d2: C).(let TMP_1 \def (Bind b) in (let TMP_2 \def (CHead d2 
+TMP_1 w) in (getl h c2 TMP_2)))) in (ex C TMP_3)))))))).