X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst1%2Ffwd.ma;h=285a870e2c1ee6b9f0a8b14b28cd6191b40bdf00;hb=7048db496643fc440aebc6e85dd425886bcd2e56;hp=2db6e6c65de685cc926d539159a2f96d39f369d3;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma
index 2db6e6c65..285a870e2 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/subst1/defs.ma".
 
-
-include "subst1/defs.ma".
-
-include "subst0/props.ma".
+include "LambdaDelta-1/subst0/props.ma".
 
 theorem subst1_gen_sort:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1 
@@ -40,7 +38,7 @@ i v (TLRef n) x) \to (or (eq T x (TLRef n)) (land (eq nat n i) (eq T x (lift
 (eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl 
 (eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O 
 v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v 
-(TLRef n) t2)).(and_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2 
+(TLRef n) t2)).(land_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2 
 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v)))) (\lambda (H1: (eq 
 nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2 
 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i)