proposition: Lemma depthImp1 : forall A B : Formula, lt_depth A (impH A B).
proof: Proof. intros A B; red; apply Nat.lt_succ_r, Nat.le_max_l. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )