(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubc/defs.ma".
+include "Basic-1/csubc/defs.ma".
theorem csubc_gen_sort_l:
\forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g (CSort n) x) \to
(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _)
\Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c2 (Bind Abbr)
w) (CHead c1 (Bind Abst) v)) H6)))))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 533
+END *)
theorem csubc_gen_head_l:
\forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (k:
g a0 c3 w0)))) c2 w a (refl_equal K (Bind Abst)) (refl_equal C (CHead c2
(Bind Abbr) w)) H14 H12 H4)) k H9))))))))) H7)) H6)))))))))))) y x H0)))
H)))))).
+(* COMMENTS
+Initial nodes: 5205
+END *)
theorem csubc_gen_sort_r:
\forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g x (CSort n)) \to
(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _)
\Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c1 (Bind Abst)
v) (CHead c2 (Bind Abbr) w)) H6)))))))))))) x y H0))) H)))).
+(* COMMENTS
+Initial nodes: 533
+END *)
theorem csubc_gen_head_r:
\forall (g: G).(\forall (c2: C).(\forall (x: C).(\forall (w: T).(\forall (k:
A).(sc3 g a0 c2 w)))) c1 v a (refl_equal K (Bind Abbr)) (refl_equal C (CHead
c1 (Bind Abst) v)) H14 H3 H12)) k H9))))))))) H7)) H6)))))))))))) x y H0)))
H)))))).
+(* COMMENTS
+Initial nodes: 5197
+END *)