proposition: Theorem or_cancel_r : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
proof: Proof. intros ? ? ? Fl Fr; split; [ | apply or_iff_compat_r]; intros [Hl Hr]; split; intros. { destruct Hl; [ left | | destruct Fl ]; assumption. } { destruct Hr; [ left | | destruct Fr ]; assumption. } Qed.
imports: Notations Ltac