bla bla bla

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / subst0 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
index c36cd597eb50c90e6fb1aeb518e9db6528d721c2..bccbf916947b9ca59d227e6070224d7828ceb08d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "subst0/fwd.ma".
-
-include "lift/props.ma".
+include "LambdaDelta-1/subst0/fwd.ma".
 
 theorem subst0_refl:
  \forall (u: T).(\forall (t: T).(\forall (d: nat).((subst0 d u t t) \to 
@@ -27,7 +25,7 @@ nat).((subst0 d u t0 t0) \to (\forall (P: Prop).P)))) (\lambda (n:
 nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TSort n) (TSort 
 n))).(\lambda (P: Prop).(subst0_gen_sort u (TSort n) d n H P))))) (\lambda 
 (n: nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TLRef n) (TLRef 
-n))).(\lambda (P: Prop).(and_ind (eq nat n d) (eq T (TLRef n) (lift (S n) O 
+n))).(\lambda (P: Prop).(land_ind (eq nat n d) (eq T (TLRef n) (lift (S n) O 
 u)) P (\lambda (_: (eq nat n d)).(\lambda (H1: (eq T (TLRef n) (lift (S n) O 
 u))).(lift_gen_lref_false (S n) O n (le_O_n n) (le_n (plus O (S n))) u H1 
 P))) (subst0_gen_lref u (TLRef n) d n H)))))) (\lambda (k: K).(\lambda (t0: 
@@ -162,7 +160,7 @@ T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda (H0: (le d i0)).(eq_ind_r T
 (plus i0 h) v (TLRef (plus i0 h)) t)) (eq_ind nat (S (plus h i0)) (\lambda 
 (n: nat).(subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift n O v))) (eq_ind_r 
 nat (plus h i0) (\lambda (n: nat).(subst0 n v (TLRef n) (lift (S (plus h i0)) 
-O v))) (subst0_lref v (plus h i0)) (plus i0 h) (plus_comm i0 h)) (plus h (S 
+O v))) (subst0_lref v (plus h i0)) (plus i0 h) (plus_sym i0 h)) (plus h (S 
 i0)) (plus_n_Sm h i0)) (lift h d (lift (S i0) O v)) (lift_free v (S i0) h O d 
 (le_S d i0 H0) (le_O_n d))) (lift h d (TLRef i0)) (lift_lref_ge i0 h d 
 H0)))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: 
@@ -215,7 +213,7 @@ t1) (lift (S O) d t2))))))))
 (plus i (S O)) (\lambda (n: nat).(subst0 n u (lift (S O) d t1) (lift (S O) d 
 t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O) 
 i) (\lambda (n: nat).(eq nat n (S i))) (refl_equal nat (S i)) (plus i (S O)) 
-(plus_comm i (S O)))))))))).
+(plus_sym i (S O)))))))))).
 
 theorem subst0_lift_ge_s:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0