proposition: Lemma eqDepth : forall A B C : Formula, depth B = depth A -> lt_depth B C -> lt_depth A C.
proof: Proof. intros A B C H; red; now rewrite <- H. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )