(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
-include "LambdaDelta-1/s/props.ma".
+include "Basic-1/s/props.ma".
theorem thead_x_lift_y_y:
\forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall
t1)) (\lambda (t2: T).(eq T t2 t1)) H4 (THead k0 (lift h d t0) (lift h (s k0
d) t1)) (lift_head k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P))))))
H3)) H2)))))))))))) t)).
+(* COMMENTS
+Initial nodes: 887
+END *)
theorem lift_r:
\forall (t: T).(\forall (d: nat).(eq T (lift O d t) t))
t1)) (\lambda (t2: T).(eq T t2 (THead k t0 t1))) (f_equal3 K T T T THead k k
(lift O d t0) t0 (lift O (s k d) t1) t1 (refl_equal K k) (H d) (H0 (s k d)))
(lift O d (THead k t0 t1)) (lift_head k t0 t1 O d)))))))) t).
+(* COMMENTS
+Initial nodes: 367
+END *)
theorem lift_lref_gt:
\forall (d: nat).(\forall (n: nat).((lt d n) \to (eq T (lift (S O) d (TLRef
(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))))))).
+(* COMMENTS
+Initial nodes: 193
+END *)
theorem lifts_tapp:
\forall (h: nat).(\forall (d: nat).(\forall (v: T).(\forall (vs: TList).(eq
(TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))))) (refl_equal TList
(TCons (lift h d t) (TApp (lifts h d t0) (lift h d v)))) (lifts h d (TApp t0
v)) H)))) vs)))).
+(* COMMENTS
+Initial nodes: 215
+END *)
theorem lift_inj:
\forall (x: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T
(THead (Flat f) t t0) t2)) (f_equal3 K T T T THead (Flat f) (Flat f) t x0 t0
x1 (refl_equal K (Flat f)) (H x0 h d H4) (H0 x1 h d H5)) t1 H3))))))
(lift_gen_flat f (lift h d t) (lift h d t0) t1 h d H2)))))))))))) k)) x).
+(* COMMENTS
+Initial nodes: 1391
+END *)
theorem lift_gen_lift:
\forall (t1: T).(\forall (x: T).(\forall (h1: nat).(\forall (h2:
H11) x1 H10)))) (H0 x1 h1 h2 d1 d2 H1 H7)) t H9) x0 H8)))) (H x0 h1 h2 d1 d2
H1 H6)) x H5)))))) (lift_gen_flat f (lift h1 d1 t) (lift h1 d1 t0) x h2 (plus
d2 h1) H4))))) k H2))))))))))))) t1).
+(* COMMENTS
+Initial nodes: 5037
+END *)
theorem lifts_inj:
\forall (xs: TList).(\forall (ts: TList).(\forall (h: nat).(\forall (d:
h d t) (lift h d t1))).(eq_ind T t (\lambda (t3: T).(eq TList (TCons t t0)
(TCons t3 t2))) (f_equal2 T TList TList TCons t t t0 t2 (refl_equal T t) (H
t2 h d H3)) t1 (lift_inj t t1 h d H4)))) H2)))))))) ts))))) xs).
+(* COMMENTS
+Initial nodes: 772
+END *)
theorem lift_free:
\forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
(THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift
h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h
d))))))))))))) t).
+(* COMMENTS
+Initial nodes: 1407
+END *)
theorem lift_d:
\forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
(lift_head k t0 t1 h d)) (lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0
(s k e) t1))) (lift_head k (lift k0 e t0) (lift k0 (s k e) t1) h (plus k0
d))) (lift k0 e (THead k t0 t1)) (lift_head k t0 t1 k0 e)))))))))))) t).
+(* COMMENTS
+Initial nodes: 2143
+END *)