[STATEMENT]
lemma irreflclpE [elim!]:
  assumes "r\<^sup>\<noteq>\<^sup>\<noteq> a b"
  obtains "r a b" "a \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r a b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r\<^sup>\<noteq>\<^sup>\<noteq> a b

goal (1 subgoal):
 1. (\<lbrakk>r a b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: irreflclp_def)