[STATEMENT]
lemma not_IndP_VarP: "{IndP x, VarP x} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
obtain m::name  where "atom m \<sharp> (x,A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. atom m \<sharp> (x, A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom m \<sharp> (x, A)

goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom m \<sharp> (x, A)

goal (1 subgoal):
 1. {IndP x, VarP x} \<turnstile> A
[PROOF STEP]
by  (auto simp: fresh_Pair) (blast intro: ExFalso cut_same [OF VarP_cong [THEN Iff_MP_same]])
[PROOF STATE]
proof (state)
this:
{IndP x, VarP x} \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed