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