proposition: Corollary dk_erase_correct `{KA: KleeneAlgebra} {env: Env}: forall n m (a b: KA.X n m), decide_kleene (erase a) (erase b) = None -> KA.eval a == KA.eval b.
proof: Proof. intros. apply erase_faithful. apply Kozen94. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)