[STATEMENT]
lemma QuoteP_subst [simp]:
  "(QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)
[PROOF STEP]
obtain s::name and k::name  where "atom s \<sharp> (t,u,w,j,k)"  "atom k \<sharp> (t,u,w,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s k. \<lbrakk>atom s \<sharp> (t, u, w, j, k); atom k \<sharp> (t, u, w, j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s \<sharp> (t, u, w, j, k)
atom k \<sharp> (t, u, w, j)

goal (1 subgoal):
 1. (QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (t, u, w, j, k)
atom k \<sharp> (t, u, w, j)

goal (1 subgoal):
 1. (QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)
[PROOF STEP]
by (simp add: QuoteP.simps [of s _ _ k])
[PROOF STATE]
proof (state)
this:
(QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Quote_0: "Quote 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quote 0 0
[PROOF STEP]
by (auto simp: Quote_def SeqQuote_def intro: BuildSeq2_exI)


[STATEMENT]
lemma QuoteP_Zero: "{} \<turnstile> QuoteP Zero Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> QuoteP Zero Zero
[PROOF STEP]
by (auto intro: Sigma_fm_imp_thm [OF QuoteP_sf]
           simp: ground_fm_aux_def supp_conv_fresh Quote_0)