X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsubv%2Ffwd.ma;h=ebc5ee5136ecbb007bf96990addf937b313de178;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=f1c483123b056164d904a4f0703e843ebc7bcbf9;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
index f1c483123..ebc5ee513 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
@@ -16,10 +16,10 @@
 
 include "basic_1/csubv/defs.ma".
 
-let rec csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: nat).(P (CSort 
-n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to ((P 
-c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind Void) v1) 
-(CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: C).(\forall (c2: 
+implied let rec csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: nat).(P 
+(CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv c1 c2) 
+\to ((P c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind Void) 
+v1) (CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: C).(\forall (c2: 
 C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not (eq B b1 Void)) 
 \to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind b1) 
 v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1: C).(\forall (c2: