(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr2/defs.ma".
+include "Basic-1/pr2/defs.ma".
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
theorem pr2_gen_sort:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TSort n) x) \to
(let H6 \def (eq_ind T t2 (\lambda (t0: T).(subst0 i u t0 t)) H3 (TSort n)
(pr0_gen_sort t2 n H5)) in (subst0_gen_sort u t i n H6 (eq T t (TSort n))))
t1 H4))))))))))))) c y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 347
+END *)
theorem pr2_gen_lref:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr2 c (TLRef n) x) \to
Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S
n) O u0)))) d u H9 (refl_equal T (lift (S n) O u))))) t H8)))
(subst0_gen_lref u t i n H6))) t1 H4))))))))))))) c y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 1003
+END *)
theorem pr2_gen_abst:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(S i) (getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 x1 H8 x3
H13)))) t H11)))))) H10)) (subst0_gen_head (Bind Abst) u x0 x1 t i H9))))))))
(pr0_gen_abst u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 2383
+END *)
theorem pr2_gen_cast:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c0 t1 t3)))) (pr2 c0 t1 t)
(pr2_delta c0 d u i H1 t1 t2 H6 t H3))) (pr0_gen_cast u1 t1 t2
H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 2659
+END *)
theorem pr2_gen_csort:
\forall (t1: T).(\forall (t2: T).(\forall (n: nat).((pr2 (CSort n) t1 t2)
(CSort n))).(let H5 \def (eq_ind C c (\lambda (c0: C).(getl i c0 (CHead d
(Bind Abbr) u))) H1 (CSort n) H4) in (getl_gen_sort n i (CHead d (Bind Abbr)
u) H5 (pr0 t3 t)))))))))))))) y t1 t2 H0))) H)))).
+(* COMMENTS
+Initial nodes: 221
+END *)
theorem pr2_gen_appl:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
x7 (s (Bind x0) i) H17)) t H15)))))) H14)) (subst0_gen_head (Bind x0) u x4
(THead (Flat Appl) (lift (S O) O x3) x5) t i H13)) t1 H8)))))))))))))) H6))
(pr0_gen_appl u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 38859
+END *)
theorem pr2_gen_abbr:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2)
H6 (lift (S O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i)))))))
(pr0_gen_abbr u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 11671
+END *)
theorem pr2_gen_void:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2) H6 (lift (S
O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i))))))) (pr0_gen_void u1 t1
t2 H5)))))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 3467
+END *)
theorem pr2_gen_lift:
\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall
(getl_drop_conf_ge i (CHead d0 (Bind Abbr) u) c0 H1 e h d H5 H11) t1 x0 H8 x1
H13))))) (subst0_gen_lift_ge u x0 t i h d H9 H11)))))))))) (pr0_gen_lift t1
t2 h d H6)))))))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1579
+END *)