proposition: Lemma iff_to_reflect {A B} (P : A -> B -> Prop) (T : A -> B -> bool) : (forall x y, T x y = true <-> P x y) -> (forall x y, reflect (P x y) (~P x y) (T x y)).
proof: Proof. intros. case_eq (T x y); intros Hxy; constructor. apply H. assumption. intros Hf. apply H in Hf. congruence. Qed.