[STATEMENT]
lemma nres_relD: "(c,a)\<in>\<langle>R\<rangle>nres_rel \<Longrightarrow> c \<le>\<Down>R a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, a) \<in> \<langle>R\<rangle>nres_rel \<Longrightarrow> c \<le> \<Down> R a
[PROOF STEP]
by (simp add: nres_rel_def)