(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/props".
+include "LambdaDelta-1/lift/fwd.ma".
-include "tlist/defs.ma".
-
-include "lift/fwd.ma".
-
-include "s/props.ma".
+include "LambdaDelta-1/s/props.ma".
theorem thead_x_lift_y_y:
\forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall
(plus (pred n) (S O))) (\lambda (t: T).(eq T t (TLRef n))) (eq_ind nat (plus
(S O) (pred n)) (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (eq_ind nat n
(\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (refl_equal T (TLRef n)) (S
-(pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_comm (S O) (pred n)))
+(pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_sym (S O) (pred n)))
(lift (S O) d (TLRef (pred n))) (lift_lref_ge (pred n) (S O) d (le_S_n d
(pred n) (eq_ind nat n (\lambda (n0: nat).(le (S d) n0)) H (S (pred n))
(S_pred n d H))))))).
t)) (refl_equal T (TLRef (plus n h1))) (lift h1 d1 (TLRef n)) (lift_lref_ge n
h1 d1 H1)) (eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t))
(refl_equal T (TLRef n)) (lift h2 d2 (TLRef n)) (lift_lref_lt n h2 d2 H3))) x
-(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (plus_lt_compat_r n d2 h1 H3) x
-H2))) (\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2:
-T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2
-t2)))) (\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2
-h1) (plus n h1) (plus_le_compat d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus
-(plus d2 h2) h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (plus_lt_compat_r n
-(plus d2 h2) h1 H4) (plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x
-H2 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T
-(TLRef n) (lift h2 d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5
-\def (eq_ind nat (plus n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2
-(plus d2 h1) x))) H2 (plus (minus (plus n h1) h2) h2) (le_plus_minus_sym h2
-(plus n h1) (le_plus_trans h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2
-h2) H4)))) in (eq_ind_r T (TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2
-T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n)
-(lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n
-h1) h2)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))
-(TLRef (minus n h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0:
-nat).(eq T (TLRef n0) (lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef
-(plus (minus n h2) h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1))
-t)) (refl_equal T (TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n
-h2))) (lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H
-(le_minus d2 n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans
-h2 (plus d2 h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2)
-h2) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2)))))
+(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (lt_reg_r n d2 h1 H3) x H2)))
+(\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2: T).(eq
+T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))
+(\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2 h1) (plus
+n h1) (le_plus_plus d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus (plus d2 h2)
+h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (lt_reg_r n (plus d2 h2) h1 H4)
+(plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x H2 (ex2 T (\lambda
+(t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2
+d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5 \def (eq_ind nat (plus
+n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 (plus d2 h1) x))) H2 (plus
+(minus (plus n h1) h2) h2) (le_plus_minus_sym h2 (plus n h1) (le_plus_trans
+h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2 h2) H4)))) in (eq_ind_r T
+(TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T
+t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))))
+(ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n h1) h2)) (lift h1
+d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef (minus n
+h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0: nat).(eq T (TLRef n0)
+(lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef (plus (minus n h2)
+h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1)) t)) (refl_equal T
+(TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n h2)))
+(lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H (le_minus d2
+n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans h2 (plus d2
+h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2) h2)
+(\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2)))))
(eq_ind_r T (TLRef (plus (minus (plus (minus n h2) h2) h2) h2)) (\lambda (t:
T).(eq T (TLRef (plus (minus n h2) h2)) t)) (f_equal nat T TLRef (plus (minus
n h2) h2) (plus (minus (plus (minus n h2) h2) h2) h2) (f_equal2 nat nat nat
(plus (minus n h2) h2) h2) (minus n h2) (minus_plus_r (minus n h2) h2))
(refl_equal nat h2))) (lift h2 d2 (TLRef (minus (plus (minus n h2) h2) h2)))
(lift_lref_ge (minus (plus (minus n h2) h2) h2) h2 d2 (le_minus d2 (plus
-(minus n h2) h2) h2 (plus_le_compat d2 (minus n h2) h2 h2 (le_minus d2 n h2
-H4) (le_n h2))))) n (le_plus_minus_sym h2 n (le_trans h2 (plus d2 h2) n
+(minus n h2) h2) h2 (le_plus_plus d2 (minus n h2) h2 h2 (le_minus d2 n h2 H4)
+(le_n h2))))) n (le_plus_minus_sym h2 n (le_trans h2 (plus d2 h2) n
(le_plus_r d2 h2) H4)))) x (lift_gen_lref_ge h2 (plus d2 h1) (minus (plus n
h1) h2) (arith0 h2 d2 n H4 h1) x H5)))))))))))))))))) (\lambda (k:
K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (h1: nat).(\forall
nat T TLRef (plus (plus n h) k) (plus n (plus k h))
(plus_permute_2_in_3_assoc n h k)) (lift (plus k h) d (TLRef n))
(lift_lref_ge n (plus k h) d H1)) (lift k e (TLRef (plus n h))) (lift_lref_ge
-(plus n h) k e (le_trans e (plus d h) (plus n h) H (plus_le_compat d n h h H1
+(plus n h) k e (le_trans e (plus d h) (plus n h) H (le_plus_plus d n h h H1
(le_n h))))) (lift h d (TLRef n)) (lift_lref_ge n h d H1))))))))))) (\lambda
(k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k0:
nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to
(plus n k)) (\lambda (t0: T).(eq T (TLRef (plus n k)) t0)) (refl_equal T
(TLRef (plus n k))) (lift k e (TLRef n)) (lift_lref_ge n k e H0)) (lift h d
(TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus d k) (TLRef (plus n k)))
-(lift_lref_lt (plus n k) h (plus d k) (plus_lt_compat_r n d k H1)))) (\lambda
-(H1: (le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T
-t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda
+(lift_lref_lt (plus n k) h (plus d k) (lt_reg_r n d k H1)))) (\lambda (H1:
+(le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T t0
+(lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda
(t0: T).(eq T (TLRef (plus (plus n k) h)) (lift k e t0))) (eq_ind_r T (TLRef
(plus (plus n h) k)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) t0))
(f_equal nat T TLRef (plus (plus n k) h) (plus (plus n h) k) (sym_eq nat
(plus (plus n h) k) (plus (plus n k) h) (plus_permute_2_in_3 n h k))) (lift k
e (TLRef (plus n h))) (lift_lref_ge (plus n h) k e (le_plus_trans e n h H0)))
(lift h d (TLRef n)) (lift_lref_ge n h d H1)) (lift h (plus d k) (TLRef (plus
-n k))) (lift_lref_ge (plus n k) h (plus d k) (plus_le_compat d n k k H1 (le_n
-k)))))) (plus k d) (plus_comm k d)) (lift k e (TLRef n)) (lift_lref_ge n k e
+n k))) (lift_lref_ge (plus n k) h (plus d k) (le_plus_plus d n k k H1 (le_n
+k)))))) (plus k d) (plus_sym k d)) (lift k e (TLRef n)) (lift_lref_ge n k e
H0)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h:
nat).(\forall (k0: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq
T (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e (lift h d