[STATEMENT]
lemma aux: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or>  (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> a; y \<noteq> b; x \<noteq> y \<and> x \<noteq> b \<or> a \<noteq> b \<and> a \<noteq> y\<rbrakk> \<Longrightarrow> {x, a} \<noteq> {y, b}
[PROOF STEP]
by (auto)