proposition: Lemma oequal_equivalence: Equivalence oequal.
proof: Proof. constructor. intros [x|]; constructor. reflexivity. intros x y [x' y' H|]; constructor. symmetry. assumption. intros x y z [x' y' H|] H'; trivial. inversion_clear H'. constructor. rewrite H. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(DecideKleeneAlgebra)