proposition: Lemma depthForall : forall (A : Formula) (v : nat), lt_depth A (forallH v A).
proof: Proof. intros A v; red; auto. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )