[STATEMENT]
lemma not_GCons_self2 [simp]: 
  fixes xs::\<Gamma>
  shows "x #\<^sub>\<Gamma> xs \<noteq> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x #\<^sub>\<Gamma> xs \<noteq> xs
[PROOF STEP]
by (rule not_GCons_self [symmetric])