(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr3/props.ma".
+include "Basic-1/pr3/props.ma".
-include "LambdaDelta-1/pr2/fwd.ma".
+include "Basic-1/pr2/fwd.ma".
theorem pr3_gen_sort:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TSort n) x) \to
T).(eq T t3 t)) (let H6 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TSort n))
\to (eq T t3 t))) H3 (TSort n) (pr2_gen_sort c t2 n H5)) in (H6 (refl_equal T
(TSort n)))) t1 H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 253
+END *)
theorem pr3_gen_abst:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
x4 x5 H12 (pr3_sing c x2 x0 H8 x4 H13) (\lambda (b: B).(\lambda (u:
T).(pr3_sing (CHead c (Bind b) u) x3 x1 (H9 b u) x5 (H14 b u))))))))))
H11)))))))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 1261
+END *)
theorem pr3_gen_cast:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c t2 x1 H7 t4
H2))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 2001
+END *)
theorem pr3_gen_lift:
\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall
(\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5)) x2
H10 (pr3_sing e x1 x0 H9 x2 H11))))) (H3 x1 H8 e H5))))) H7))))))))))))) y x
H0)))) H)))))).
+(* COMMENTS
+Initial nodes: 689
+END *)
theorem pr3_gen_lref:
\forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TLRef n) x) \to
C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda
(_: T).(\lambda (v: T).(eq T t3 (lift (S n) O v))))) x0 x1 x2 H8 H14 H13)))))
H12)))))))) H7)) H6)) t1 H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 1515
+END *)
theorem pr3_gen_void:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
(pr3_sing (CHead c (Bind Void) x0) (lift (S O) O t2) x1 (H7 Void x0) (lift (S
O) O t4) (pr3_lift (CHead c (Bind Void) x0) c (S O) O (drop_drop (Bind Void)
O c c (drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 2645
+END *)
theorem pr3_gen_abbr:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
(CHead c (Bind Abbr) x0) (lift (S O) O t2) x1 (H7 Abbr x0) (lift (S O) O t4)
(pr3_lift (CHead c (Bind Abbr) x0) c (S O) O (drop_drop (Bind Abbr) O c c
(drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 5983
+END *)
theorem pr3_gen_appl:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
y2) z1 z2))))))) x2 x3 x4 x5 x6 x7 H8 (pr3_refl c (THead (Bind x2) x3 x4))
H15 (pr3_pr2 c x0 x6 H11) (pr3_pr2 c x3 x7 H12) (pr3_pr2 (CHead c (Bind x2)
x7) x4 x5 H13))))) x1 H9))))))))))))) H7)) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 12691
+END *)
theorem pr3_gen_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u1:
T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void) u1) t1
t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)) H2)) H1)))))))) b).
+(* COMMENTS
+Initial nodes: 1721
+END *)