[STATEMENT]
lemma refl_joinable_iff: "(\<forall>x. \<exists>y. (x, y) \<in> R) = refl (joinable R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. \<exists>y. (x, y) \<in> R) = refl (joinable R)
[PROOF STEP]
by (auto intro!: refl_onI dest: refl_onD simp add: joinable_simp)