(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/defs.ma".
+include "Basic-1/csubt/defs.ma".
theorem csubt_gen_abbr:
\forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csubt g
_) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H5) in (False_ind (ex2 C
(\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v)))
(\lambda (e2: C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 1111
+END *)
theorem csubt_gen_abst:
\forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csubt g
g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
C).(\lambda (v2: T).(ty3 g e2 v2 v1))) c3 u (refl_equal C (CHead c3 (Bind
Abbr) u)) H13 H11 H9))))))))) H6))))))))))) y c2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 2362
+END *)
theorem csubt_gen_flat:
\forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).(\forall
False])])) I (CHead e1 (Flat f) v) H5) in (False_ind (ex2 C (\lambda (e2:
C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Flat f) v))) (\lambda (e2:
C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1103
+END *)
theorem csubt_gen_bind:
\forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
(Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g
e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H15))))))))))
H7)) H6))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1899
+END *)