proposition: Theorem and_tiff_compat_l: forall A B C : [univ], (B <=> C) -> (A # B <=> A # C).
proof: Proof. introv Hiff. rw Hiff. apply t_iff_refl. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega