[STATEMENT]
lemma par_neq1:
  assumes "A B Par C D"
  shows "A \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> B
[PROOF STEP]
using Par_def assms par_strict_neq1
[PROOF STATE]
proof (prove)
using this:
?A ?B Par ?C ?D \<equiv> ?A ?B ParStrict ?C ?D \<or> ?A \<noteq> ?B \<and> ?C \<noteq> ?D \<and> Col ?A ?C ?D \<and> Col ?B ?C ?D
A B Par C D
?A ?B ParStrict ?C ?D \<Longrightarrow> ?A \<noteq> ?B

goal (1 subgoal):
 1. A \<noteq> B
[PROOF STEP]
by blast