proposition: Lemma impl_to_semireflect {A B} (P : A -> B -> Prop) (T : A -> B -> bool) : (forall x y, T x y = true -> P x y) -> (forall x y, semi_reflect (P x y) (T x y)).
proof: Proof. intros. case_eq (T x y); intros Hxy; constructor. apply H; auto. Qed.