(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csuba/defs.ma".
+include "Basic-1/csuba/defs.ma".
theorem csuba_gen_abbr:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u0)
(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) H6))))))))))))
y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 1117
+END *)
theorem csuba_gen_void:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind b) u2)))))
(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))
H6)))))))))))) y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 1418
+END *)
theorem csuba_gen_abst:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
a0)))) c2 u a (refl_equal C (CHead c2 (Bind Abbr) u)) H12 H10 H4))))))))
H6)))))))))))) y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 2550
+END *)
theorem csuba_gen_flat:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
(Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))
H6)))))))))))) y c H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1183
+END *)
theorem csuba_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).(csuba g
e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H14))))))))) H7))
H6)))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1889
+END *)
theorem csuba_gen_abst_rev:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind
Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
g d2 d1))))) H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 1980
+END *)
theorem csuba_gen_void_rev:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
d1 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
(Bind Abst) t) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))
H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 1326
+END *)
theorem csuba_gen_abbr_rev:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c
(asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1
u1 a0)))) c1 t a (refl_equal C (CHead c1 (Bind Abst) t)) H12 H3 H10))))))))
H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 3459
+END *)
theorem csuba_gen_flat_rev:
\forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2
(Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
H6)))))))))))) c y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1183
+END *)
theorem csuba_gen_bind_rev:
\forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))
Abst c1 t (refl_equal C (CHead c1 (Bind Abst) t)) H14))))))))) H7))
H6)))))))))))) c2 y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1831
+END *)