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