(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/props".
-
-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
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:
(lift h d u1) (lift h d u2) i0 (H1 d H4 h) k (lift h (s k d) t0) (lift h (s k
d) t3) (eq_ind nat (minus (s k d) (s k (S i0))) (\lambda (n: nat).(subst0 (s
k i0) (lift h n v) (lift h (s k d) t0) (lift h (s k d) t3))) (H5 (s k d)
-(lt_le_S (s k i0) (s k d) (s_lt k i0 d H4)) h) (minus d (S i0)) (minus_s_s k
-d (S i0)))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d
-(THead k u1 t0)) (lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
+(s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d
+(THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0))
+(lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
theorem subst0_lift_ge:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall
(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:
(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