proposition: Lemma Formula_depth_ind2 : forall P : Formula -> Prop, (forall t t0 : Term, P (equal t t0)) -> (forall (r : Relations L) (t : Terms (arityR L r)), P (atomic r t)) -> (forall f : Formula, P f -> forall f0 : Formula, P f0 -> P (impH f f0)) -> (forall f : Formula, P f -> P (notH f)) -> (forall (v : nat) (a : Formula), (forall b : Formula, lt_depth b (forallH v a) -> P b) -> P (forallH v a)) -> forall f : Formula, P f.
proof: Proof. intros P H H0 H1 H2 H3 f; apply Formula_depth_ind. simple induction a; auto. - intros f0 H4 f1 H5 H6; apply H1. + apply H6, depthImp1. + apply H6, depthImp2. - intros f0 H4 H5; apply H2, H5. apply depthNot. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )