[STATEMENT]
lemma ptrm_prm_agreement_equiv:
  assumes "\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M"
  shows "\<pi> \<bullet> M \<approx> \<sigma> \<bullet> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs M

goal (1 subgoal):
 1. \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M
[PROOF STEP]
proof(induction M arbitrary: \<pi> \<sigma>)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs PUnit) \<Longrightarrow> \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
 2. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 4. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 5. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 7. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PUnit)
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit

goal (7 subgoals):
 1. \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs PUnit) \<Longrightarrow> \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
 2. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 4. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 5. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 7. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit

goal (1 subgoal):
 1. \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
[PROOF STEP]
using ptrm_alpha_equiv.unit
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit
PUnit \<approx> PUnit

goal (1 subgoal):
 1. \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PVar x)
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PVar x)

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
consider "x \<in> ds \<pi> \<sigma>" | "x \<notin> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<in> ds \<pi> \<sigma>

goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
hence "x \<notin> ptrm_fvs (PVar x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<notin> ptrm_fvs (PVar x)
[PROOF STEP]
using PVar.prems
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PVar x)

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

goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> ptrm_fvs (PVar x)

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
hence "\<pi> $ x = \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
using prm_disagreement_ext
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x = \<sigma> $ x

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x = \<sigma> $ x

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
using ptrm_alpha_equiv.var
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x = \<sigma> $ x
PVar ?x \<approx> PVar ?x

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PApp A B)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PApp A B)

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A" and "\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PApp A B)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> \<sigma> \<bullet> A &&& \<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (1 subgoal):
 1. \<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B
[PROOF STEP]
using ptrm_alpha_equiv.app
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
\<lbrakk>?A \<approx> ?B; ?C \<approx> ?D\<rbrakk> \<Longrightarrow> PApp ?A ?C \<approx> PApp ?B ?D

goal (1 subgoal):
 1. \<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PFn x T A)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
consider "x \<notin> ds \<pi> \<sigma>" | "x \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<notin> ds \<pi> \<sigma>

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
hence *: "\<pi> $ x = \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
using prm_disagreement_ext
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x = \<sigma> $ x

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
assume "a \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<notin> ptrm_fvs (PFn x T A)"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs (PFn x T A)
[PROOF STEP]
using PFn.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a \<notin> ptrm_fvs (PFn x T A)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a = x \<or> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a = x \<or> a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x \<or> a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
thus "a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a = x \<or> a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
using \<open>a \<in> ds \<pi> \<sigma>\<close> \<open>x \<notin> ds \<pi> \<sigma>\<close>
[PROOF STATE]
proof (prove)
using this:
a = x \<or> a \<notin> ptrm_fvs A
a \<in> ds \<pi> \<sigma>
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
using PFn.IH * ptrm_alpha_equiv.fn1 ptrm_apply_prm.simps(3)
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
\<pi> $ x = \<sigma> $ x
?A \<approx> ?B \<Longrightarrow> PFn ?x ?T ?A \<approx> PFn ?x ?T ?B
?\<pi> \<bullet> PApp ?A ?B = PApp (?\<pi> \<bullet> ?A) (?\<pi> \<bullet> ?B)

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
hence "\<pi> $ x \<noteq> \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x \<noteq> \<sigma> $ x
[PROOF STEP]
using prm_disagreement_def CollectD
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>
ds ?\<pi> ?\<sigma> \<equiv> {x. ?\<pi> $ x \<noteq> ?\<sigma> $ x}
?a \<in> {x. ?P x} \<Longrightarrow> ?P ?a

goal (1 subgoal):
 1. \<pi> $ x \<noteq> \<sigma> $ x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
have "y \<in> (ptrm_fvs A) \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y
[PROOF STEP]
using PFn \<open>\<pi> $ x \<noteq> \<sigma> $ x\<close> prm_apply_unequal prm_disagreement_ext ptrm_fvs.simps(4)
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)
\<pi> $ x \<noteq> \<sigma> $ x
?x \<noteq> ?y \<Longrightarrow> ?\<pi> $ ?x \<noteq> ?\<pi> $ ?y
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
ptrm_fvs (PFn ?x ?uu ?A) = ptrm_fvs ?A - {?x}

goal (1 subgoal):
 1. y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y
[PROOF STEP]
by (metis Diff_iff empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
hence "\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A
[PROOF STEP]
unfolding prm_set_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> ($) \<sigma> ` ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
using ptrm_prm_fvs
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A
ptrm_fvs (?\<pi> \<bullet> ?X) = ?\<pi> {$} ptrm_fvs ?X

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
have "\<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
assume *: "a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)"
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)

goal (1 subgoal):
 1. a \<noteq> x
[PROOF STEP]
using \<open>\<pi> $ x \<noteq> \<sigma> $ x\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. a \<noteq> x
[PROOF STEP]
using prm_apply_composition prm_disagreement_ext prm_unit_action prm_unit_commutes
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
\<pi> $ x \<noteq> \<sigma> $ x
?f \<diamondop> ?g $ ?x = ?f $ (?g $ ?x)
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
[?a \<leftrightarrow> ?b] $ ?a = ?b
[?a \<leftrightarrow> ?b] = [?b \<leftrightarrow> ?a]

goal (1 subgoal):
 1. a \<noteq> x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<noteq> x

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x

goal (1 subgoal):
 1. a \<in> ds \<pi> \<sigma>
[PROOF STEP]
using * prm_apply_composition prm_apply_unequal prm_disagreement_ext prm_unit_inaction
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
?f \<diamondop> ?g $ ?x = ?f $ (?g $ ?x)
?x \<noteq> ?y \<Longrightarrow> ?\<pi> $ ?x \<noteq> ?\<pi> $ ?y
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
\<lbrakk>?x \<noteq> ?a; ?x \<noteq> ?b\<rbrakk> \<Longrightarrow> [?a \<leftrightarrow> ?b] $ ?x = ?x

goal (1 subgoal):
 1. a \<in> ds \<pi> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
thus "a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
using \<open>a \<noteq> x\<close> PFn.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>
a \<noteq> x
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
using PFn
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
by (simp add: ptrm_prm_apply_compose)
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
using ptrm_alpha_equiv.fn2
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
\<lbrakk>?a \<noteq> ?b; ?A \<approx> [?a \<leftrightarrow> ?b] \<bullet> ?B; ?a \<notin> ptrm_fvs ?B\<rbrakk> \<Longrightarrow> PFn ?a ?T ?A \<approx> PFn ?b ?T ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PPair A B)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PPair A B)

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A" and "\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PPair A B)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> \<sigma> \<bullet> A &&& \<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (1 subgoal):
 1. \<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B
[PROOF STEP]
using ptrm_alpha_equiv.pair
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
\<lbrakk>?A \<approx> ?B; ?C \<approx> ?D\<rbrakk> \<Longrightarrow> PPair ?A ?C \<approx> PPair ?B ?D

goal (1 subgoal):
 1. \<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PFst P)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFst P)

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFst P)

goal (1 subgoal):
 1. \<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P
[PROOF STEP]
using ptrm_alpha_equiv.fst
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
?A \<approx> ?B \<Longrightarrow> PFst ?A \<approx> PFst ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PSnd P)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PSnd P)

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PSnd P)

goal (1 subgoal):
 1. \<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P
[PROOF STEP]
using ptrm_alpha_equiv.snd
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
?A \<approx> ?B \<Longrightarrow> PSnd ?A \<approx> PSnd ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed