378   and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"

   378   and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"

   379 proof -

   379 proof -

   380   show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"

   380   show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"

   381   and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"

   381   and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"

   382   and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"

   382   and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"

   384     apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)

   383     apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)

   385     by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)

   384     by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)

   386 qed

   385 qed

   387 

   386 

   388 lemma fresh_fact_mix:

   387 lemma fresh_fact_mix: