(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/lift/defs.ma".
+include "Basic-1/lift/defs.ma".
theorem lift_sort:
\forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort
\def
\lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort
n)))).
+(* COMMENTS
+Initial nodes: 13
+END *)
theorem lift_lref_lt:
\forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T
d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true
\Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T
(TLRef n)) (blt n d) (sym_eq bool (blt n d) true (lt_blt d n H)))))).
+(* COMMENTS
+Initial nodes: 72
+END *)
theorem lift_lref_ge:
\forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T
\Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h))))
(refl_equal T (TLRef (plus n h))) (blt n d) (sym_eq bool (blt n d) false
(le_bge d n H)))))).
+(* COMMENTS
+Initial nodes: 80
+END *)
theorem lift_head:
\forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
\def
\lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
(d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).
+(* COMMENTS
+Initial nodes: 37
+END *)
theorem lift_bind:
\forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
\def
\lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
(d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).
+(* COMMENTS
+Initial nodes: 37
+END *)
theorem lift_flat:
\forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
\def
\lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
(d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).
+(* COMMENTS
+Initial nodes: 35
+END *)
theorem lift_gen_sort:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).(\forall (t: T).((eq T
True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
(THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (eq T (THead k
t0 t1) (TSort n)) H3))))))))) t)))).
+(* COMMENTS
+Initial nodes: 613
+END *)
theorem lift_gen_lref:
\forall (t: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T
t1)) H2) in (False_ind (or (land (lt i d) (eq T (THead k t0 t1) (TLRef i)))
(land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))))
H3)))))))))))) t).
+(* COMMENTS
+Initial nodes: 1221
+END *)
theorem lift_gen_lref_lt:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).((lt n d) \to (\forall
(minus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq
T (TLRef (minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S
n) d h H))) t H4))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 363
+END *)
theorem lift_gen_lref_false:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n
h))))).(land_ind (le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda
(H4: (le (plus d h) n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false
(plus d h) n P H4 H0))) H3)) H2)))))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
theorem lift_gen_lref_ge:
\forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall
(H4: (eq T t (TLRef (minus (plus n h) h)))).(eq_ind_r T (TLRef (minus (plus n
h) h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (minus
(plus n h) h) n (minus_plus_r n h)) t H4))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 473
+END *)
theorem lift_gen_head:
\forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
z)))) t0 t1 (refl_equal T (THead k t0 t1)) (refl_equal T (lift h d t0))
(refl_equal T (lift h (s k d) t1))) u H6))) t H8))) k0 H7))))) H4))
H3))))))))))) x)))).
+(* COMMENTS
+Initial nodes: 2083
+END *)
theorem lift_gen_bind:
\forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d)
z)))) x0 x1 (refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d
x0)) (refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
+(* COMMENTS
+Initial nodes: 637
+END *)
theorem lift_gen_flat:
\forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
(lift h d x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat f) x0 x1))
(refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t H3) x
H1)))))) H0))))))))).
+(* COMMENTS
+Initial nodes: 615
+END *)