proposition: Lemma translate_correct: forall ce, translate_ce ce = None <-> ce = None.
proof: Proof. intros [[b w]|]; simpl; intuition discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)