(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wcpr0/defs.ma".
+include "Basic-1/wcpr0/defs.ma".
theorem wcpr0_gen_sort:
\forall (x: C).(\forall (n: nat).((wcpr0 (CSort n) x) \to (eq C x (CSort
with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
(CSort n) H4) in (False_ind (eq C (CHead c2 k u2) (CHead c1 k u1))
H5))))))))))) y x H0))) H))).
+(* COMMENTS
+Initial nodes: 249
+END *)
theorem wcpr0_gen_head:
\forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).((wcpr0
c1 c3))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) c2 u2 (refl_equal C
(CHead c2 k u2)) H12 H10)) c0 H9))) u0 H7)) k0 H8)))) H6)) H5))))))))))) y x
H0))) H))))).
+(* COMMENTS
+Initial nodes: 1133
+END *)