(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
-include "LambdaDelta-1/drop1/defs.ma".
+include "Basic-1/drop1/defs.ma".
theorem lift1_lift1:
\forall (is1: PList).(\forall (is2: PList).(\forall (t: T).(eq T (lift1 is1
(papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t: T).(f_equal3 nat nat
T T lift n n n0 n0 (lift1 p (lift1 is2 t)) (lift1 (papp p is2) t) (refl_equal
nat n) (refl_equal nat n0) (H is2 t)))))))) is1).
+(* COMMENTS
+Initial nodes: 145
+END *)
theorem lift1_xhg:
\forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t))
(S O) O (lift h d (lift1 p t)))) (lift h (plus (S O) d) (lift (S O) O (lift1
p t))) (lift_d (lift1 p t) h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S
d))) (lift1 (Ss p) (lift (S O) O t)) (H t))))))) hds).
+(* COMMENTS
+Initial nodes: 371
+END *)
theorem lifts1_xhg:
\forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (Ss hds) (lifts
t0))))) (refl_equal TList (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O
(lifts1 hds t0)))) (lifts1 (Ss hds) (lifts (S O) O t0)) H) (lift1 (Ss hds)
(lift (S O) O t)) (lift1_xhg hds t))))) ts)).
+(* COMMENTS
+Initial nodes: 307
+END *)
theorem lift1_free:
\forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds
(plus_sym O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans
hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O t)) (H i t))))))))
hds).
+(* COMMENTS
+Initial nodes: 1339
+END *)