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