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