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