[STATEMENT]
lemma Eats_Mem_sf:
  assumes "\<And>j::name. Sigma_fm (Var j EQ t)"
      and "\<And>k::name. Sigma_fm (Var k EQ u)"
  shows "Sigma_fm (Eats t u IN Var i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
obtain j::name where j: "atom j \<sharp> (t,u,Var i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. atom j \<sharp> (t, u, Var i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (t, u, Var i)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
hence "{} \<turnstile> Eats t u IN Var i IFF
              Ex j (Var j IN Var i AND Var j EQ Eats t u)"
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (t, u, Var i)

goal (1 subgoal):
 1. {} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)
[PROOF STEP]
apply (auto simp: fresh_Pair intro: Ex_I [where x="Eats t u"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> t; atom j \<sharp> u; atom j \<sharp> i\<rbrakk> \<Longrightarrow> {Var j IN Var i, Var j EQ Eats t u} \<turnstile> Eats t u IN Var i
[PROOF STEP]
apply (metis Assume Mem_cong [OF _ Refl, THEN Iff_MP_same] rotate2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
by (rule Sigma_fm_Iff) (auto simp: assms supp_conv_fresh Eq_Eats_sf)
[PROOF STATE]
proof (state)
this:
Sigma_fm (Eats t u IN Var i)

goal:
No subgoals!
[PROOF STEP]
qed