(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr0/props.ma".
+include "Basic-1/pr0/props.ma".
theorem pr0_gen_sort:
\forall (x: T).(\forall (n: nat).((pr0 (TSort n) x) \to (eq T x (TSort n))))
False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
(TSort n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x
H0))) H))).
+(* COMMENTS
+Initial nodes: 1045
+END *)
theorem pr0_gen_lref:
\forall (x: T).(\forall (n: nat).((pr0 (TLRef n) x) \to (eq T x (TLRef n))))
False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
(TLRef n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x
H0))) H))).
+(* COMMENTS
+Initial nodes: 1045
+END *)
theorem pr0_gen_abst:
\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abst) u1
t1) H3) in (False_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
(THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
(\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 2838
+END *)
theorem pr0_gen_appl:
\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Appl) u1
T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
(t3: T).(pr0 z1 t3))))))))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 12299
+END *)
theorem pr0_gen_cast:
\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Cast) u1
(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3))))
(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
T).(pr0 t1 t3)))) (pr0 t1 t2) H8))))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 2911
+END *)
theorem pr0_gen_abbr:
\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1
T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
(\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))
H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 4711
+END *)
theorem pr0_gen_void:
\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1
u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2))) H4)))))))) y x
H0))) H)))).
+(* COMMENTS
+Initial nodes: 3436
+END *)
theorem pr0_gen_lift:
\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((pr0
Cast) x2 x3) t4)) x4 (refl_equal T (lift h x1 x4)) (pr0_tau x3 x4 H7 x2)) t3
H_x)))) (H2 x3 x1 H6)) x0 H4)))))) (lift_gen_flat Cast u t2 x0 h x1
H3)))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 7569
+END *)