fact: Fixpoint depth (A : Formula) : nat := match A with | equal _ _ => 0 | atomic _ _ => 0 | impH A B => S (Nat.max (depth A) (depth B)) | notH A => S (depth A) | forallH _ A => S (depth A) end.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )