(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/arity/defs.ma".
+include "Basic-1/arity/defs.ma".
-include "LambdaDelta-1/leq/asucc.ma".
+include "Basic-1/leq/asucc.ma".
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
theorem arity_gen_sort:
\forall (g: G).(\forall (c: C).(\forall (n: nat).(\forall (a: A).((arity g c
T).(arity g c0 t0 a1)) H1 (TSort n) H5) in (leq_trans g a2 a1 (leq_sym g a1
a2 H3) (ASort O n) (H6 (refl_equal T (TSort n))))))))))))))) c y a H0)))
H))))).
+(* COMMENTS
+Initial nodes: 1235
+END *)
theorem arity_gen_lref:
\forall (g: G).(\forall (c: C).(\forall (i: nat).(\forall (a: A).((arity g c
(CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u
(asucc g a2)))) x0 x1 H10 (arity_repl g x0 x1 (asucc g a1) H11 (asucc g a2)
(asucc_repl g a1 a2 H3)))))))) H9)) H8))))))))))))) c y a H0))) H))))).
+(* COMMENTS
+Initial nodes: 3853
+END *)
theorem arity_gen_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (g: G).(\forall (c:
c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a0)) x H10
(arity_repl g (CHead c0 (Bind b) u) t a1 H11 a0 H4))))) H9))))))))))))) c y
a2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 3365
+END *)
theorem arity_gen_abst:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a:
x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) (asucc_repl g x0 x2
H15)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H16)) a2 H18)))))))
H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
+(* COMMENTS
+Initial nodes: 4265
+END *)
theorem arity_gen_appl:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a2:
u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 a0))) x H9 (arity_repl g c0 t
(AHead x a1) H10 (AHead x a0) (leq_head g x x (leq_refl g x) a1 a0 H3))))))
H8))))))))))))) c y a2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2277
+END *)
theorem arity_gen_cast:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a:
a1)).(conj (arity g c0 u (asucc g a2)) (arity g c0 t a2) (arity_repl g c0 u
(asucc g a1) H9 (asucc g a2) (asucc_repl g a1 a2 H3)) (arity_repl g c0 t a1
H10 a2 H3)))) H8))))))))))))) c y a H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2147
+END *)
theorem arity_gen_appls:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (vs: TList).(\forall
(\lambda (a: A).(arity g c t a)) (ex A (\lambda (a: A).(arity g c t a)))
(\lambda (x0: A).(\lambda (H5: (arity g c t x0)).(ex_intro A (\lambda (a:
A).(arity g c t a)) x0 H5))) H4)))))) H1))))))) vs)))).
+(* COMMENTS
+Initial nodes: 341
+END *)
theorem arity_gen_lift:
\forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).(\forall (h:
a2)).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T t0 (lift h x
x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(arity_repl g c2 x0 a1
(H2 x x0 H4 c2 H5) a2 H3))))))))))))) c1 y a H0))))) H))))))).
+(* COMMENTS
+Initial nodes: 4693
+END *)