proposition: Lemma rel_rel_to_fun_of_not_forall : forall R a, ~ (forall b, ~ R a b) -> R a (rel_to_fun R a).
proof: Proof. Proof using IB. introv. rew_logic. intros [x H]. applys* rel_rel_to_fun_of_exists. Qed.
imports: TLC(LibTactics LibLogic LibRelation)