fact: Definition Formula_depth_rec2 (P : Formula -> Set) (f1 : forall t t0 : Term, P (equal t t0)) (f2 : forall (r : Relations L) (t : Terms (arityR L r)), P (atomic r t)) (f3 : forall f : Formula, P f -> forall f0 : Formula, P f0 -> P (impH f f0)) (f4 : forall f : Formula, P f -> P (notH f)) (f5 : forall (v : nat) (a : Formula), (forall b : Formula, lt_depth b (forallH v a) -> P b) -> P (forallH v a)) (a : Formula) : P a := Formula_depth_rec P (Formula_depth_rec2rec P f1 f2 f3 f4 f5) a.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )