[STATEMENT]
lemma unit_not_var:
  shows "Unit \<noteq> Var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Unit \<noteq> Var x
[PROOF STEP]
proof(transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<not> PUnit \<approx> PVar x
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<not> PUnit \<approx> PVar x
[PROOF STEP]
show "\<not> PUnit \<approx> PVar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> PUnit \<approx> PVar x
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
assume "\<not>\<not> PUnit \<approx> PVar x"
[PROOF STATE]
proof (state)
this:
\<not> \<not> PUnit \<approx> PVar x

goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> PUnit \<approx> PVar x

goal (1 subgoal):
 1. False
[PROOF STEP]
using unitE
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> PUnit \<approx> PVar x
\<lbrakk>PUnit \<approx> ?Y; ?Y = PUnit \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> \<not> PUnit \<approx> PVar x \<Longrightarrow> \<not> PUnit \<approx> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<not> PUnit \<approx> PVar x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> PUnit \<approx> PVar x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> PUnit \<approx> PVar x

goal:
No subgoals!
[PROOF STEP]
qed