[STATEMENT]
lemma ID_combination_subset_union [intro]:
  "RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>"
  "LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau> &&& LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
 2. LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
show "RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
assume "r \<in> RID\<^sub>S (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma>;;\<tau>)

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
r \<in> RID\<^sub>S (\<sigma>;;\<tau>)
[PROOF STEP]
obtain l v where "(\<sigma>;;\<tau>) l = Some v" and "r \<in> RID\<^sub>V v"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<sigma>;;\<tau>)

goal (1 subgoal):
 1. (\<And>l v. \<lbrakk>(\<sigma>;;\<tau>) l = Some v; r \<in> RID\<^sub>V v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>;;\<tau>) l = Some v
r \<in> RID\<^sub>V v

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
thus "r \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>;;\<tau>) l = Some v
r \<in> RID\<^sub>V v

goal (1 subgoal):
 1. r \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>
[PROOF STEP]
by (cases "l \<in> dom \<tau>") auto
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau>

goal (1 subgoal):
 1. LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
show "LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
assume "l \<in> LID\<^sub>S (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>S (\<sigma>;;\<tau>)

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
hence "l \<in> dom (\<sigma>;;\<tau>) \<or> (\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>S (\<sigma>;;\<tau>)

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>) \<or> (\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>) \<or> (\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v)

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
thus "l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
using this:
l \<in> dom (\<sigma>;;\<tau>) \<or> (\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v)

goal (1 subgoal):
 1. l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l \<in> dom (\<sigma>;;\<tau>) \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
 2. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
assume "l \<in> dom (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>)

goal (2 subgoals):
 1. l \<in> dom (\<sigma>;;\<tau>) \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
 2. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
thus "l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
using this:
l \<in> dom (\<sigma>;;\<tau>)

goal (1 subgoal):
 1. l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
by (cases "l \<in> dom \<tau>") auto
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>

goal (1 subgoal):
 1. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
assume "\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v"
[PROOF STATE]
proof (state)
this:
\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v

goal (1 subgoal):
 1. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v
[PROOF STEP]
obtain l' v where "(\<sigma>;;\<tau>) l' = Some v" "l \<in> LID\<^sub>V v"
[PROOF STATE]
proof (prove)
using this:
\<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v

goal (1 subgoal):
 1. (\<And>l' v. \<lbrakk>(\<sigma>;;\<tau>) l' = Some v; l \<in> LID\<^sub>V v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>;;\<tau>) l' = Some v
l \<in> LID\<^sub>V v

goal (1 subgoal):
 1. \<exists>l' v. (\<sigma>;;\<tau>) l' = Some v \<and> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
thus "l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>;;\<tau>) l' = Some v
l \<in> LID\<^sub>V v

goal (1 subgoal):
 1. l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>
[PROOF STEP]
by (cases "l' \<in> dom \<tau>") auto
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LID\<^sub>S (\<sigma>;;\<tau>) \<subseteq> LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_combination_in_component [intro]:
  "r \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> r \<notin> RID\<^sub>S \<sigma> \<Longrightarrow> r \<in> RID\<^sub>S \<tau>"
  "r \<in> RID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> r \<notin> RID\<^sub>S \<tau> \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>"
  "l \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> l \<notin> LID\<^sub>S \<sigma> \<Longrightarrow> l \<in> LID\<^sub>S \<tau>"
  "l \<in> LID\<^sub>S (\<sigma>;;\<tau>) \<Longrightarrow> l \<notin> LID\<^sub>S \<tau> \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>r \<in> RID\<^sub>S (\<sigma>;;\<tau>); r \<notin> RID\<^sub>S \<sigma>\<rbrakk> \<Longrightarrow> r \<in> RID\<^sub>S \<tau>) &&& (\<lbrakk>r \<in> RID\<^sub>S (\<sigma>;;\<tau>); r \<notin> RID\<^sub>S \<tau>\<rbrakk> \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>)) &&& (\<lbrakk>l \<in> LID\<^sub>S (\<sigma>;;\<tau>); l \<notin> LID\<^sub>S \<sigma>\<rbrakk> \<Longrightarrow> l \<in> LID\<^sub>S \<tau>) &&& (\<lbrakk>l \<in> LID\<^sub>S (\<sigma>;;\<tau>); l \<notin> LID\<^sub>S \<tau>\<rbrakk> \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>)
[PROOF STEP]
by (meson Un_iff ID_combination_subset_union subsetCE)+


[STATEMENT]
lemma in_mapped_in_component_of_combination [intro]:
  assumes
    maps_to_v: "(\<sigma>;;\<tau>) l = Some v" and
    l'_in_v: "l' \<in> LID\<^sub>V v"
  shows
    "l' \<notin> LID\<^sub>S \<tau> \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>"
    "l' \<notin> LID\<^sub>S \<sigma> \<Longrightarrow> l' \<in> LID\<^sub>S \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l' \<notin> LID\<^sub>S \<tau> \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>) &&& (l' \<notin> LID\<^sub>S \<sigma> \<Longrightarrow> l' \<in> LID\<^sub>S \<tau>)
[PROOF STEP]
by (metis LID\<^sub>SI(2) combine.simps l'_in_v maps_to_v)+


[STATEMENT]
lemma elim_trivial_restriction [simp]: "l \<notin> LID\<^sub>S \<tau> \<Longrightarrow> (\<tau>(l := None)) = \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<notin> LID\<^sub>S \<tau> \<Longrightarrow> \<tau>(l := None) = \<tau>
[PROOF STEP]
by (simp add: LID\<^sub>S_def domIff fun_upd_idem)


[STATEMENT]
lemma ID_distr_global_conditional:
  "s r = Some ls \<Longrightarrow> RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)"
  "s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s r = Some ls \<Longrightarrow> RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)) &&& (s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s r = Some ls \<Longrightarrow> RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
 2. s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
assume "s r = Some ls"
[PROOF STATE]
proof (state)
this:
s r = Some ls

goal (2 subgoals):
 1. s r = Some ls \<Longrightarrow> RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
 2. s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
hence s_as_upd: "s = (s(r \<mapsto> ls))"
[PROOF STATE]
proof (prove)
using this:
s r = Some ls

goal (1 subgoal):
 1. s = s(r \<mapsto> ls)
[PROOF STEP]
by (simp add: fun_upd_idem)
[PROOF STATE]
proof (state)
this:
s = s(r \<mapsto> ls)

goal (2 subgoals):
 1. s r = Some ls \<Longrightarrow> RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
 2. s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
show "RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
[PROOF STEP]
by (subst s_as_upd, simp)
[PROOF STATE]
proof (state)
this:
RID\<^sub>G s = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)

goal (1 subgoal):
 1. s r = Some ls \<Longrightarrow> LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
show "LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
by (subst s_as_upd, simp)
[PROOF STATE]
proof (state)
this:
LID\<^sub>G s = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code]: \<open>Stream.smember x (y ## s) = (x = y \<or> Stream.smember x s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Stream.smember x (y ## s) = (x = y \<or> Stream.smember x s)
[PROOF STEP]
unfolding Stream.smember_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> i.R (y ## s)) = (x = y \<or> x \<in> i.R s)
[PROOF STEP]
by auto


[STATEMENT]
lemma liftL_type:
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> \<forall>k. \<Gamma>\<langle>k:U\<rangle>, \<Delta> \<turnstile>\<^sub>T (liftL_trm t k) : T"
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> \<forall>k. \<Gamma>\<langle>k:U\<rangle>, \<Delta> \<turnstile>\<^sub>C (liftL_cmd c k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> \<forall>k. \<Gamma>\<langle>k:U\<rangle> , \<Delta> \<turnstile>\<^sub>T liftL_trm t k : T) &&& (\<Gamma> , \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> \<forall>k. \<Gamma>\<langle>k:U\<rangle> , \<Delta> \<turnstile>\<^sub>C liftL_cmd c k)
[PROOF STEP]
by (induct rule: typing_trm_typing_cmd.inducts) auto


[STATEMENT]
lemma liftM_type:
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> \<forall>k. \<Gamma>, \<Delta>\<langle>k:U\<rangle> \<turnstile>\<^sub>T (liftM_trm t k) : T"
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> \<forall>k. \<Gamma>, \<Delta>\<langle>k:U\<rangle> \<turnstile>\<^sub>C (liftM_cmd c k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> \<forall>k. \<Gamma> , \<Delta>\<langle>k:U\<rangle> \<turnstile>\<^sub>T liftM_trm t k : T) &&& (\<Gamma> , \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> \<forall>k. \<Gamma> , \<Delta>\<langle>k:U\<rangle> \<turnstile>\<^sub>C liftM_cmd c k)
[PROOF STEP]
by(induct rule: typing_trm_typing_cmd.inducts) auto


[STATEMENT]
lemma dropM_type:
  "\<Gamma> , \<Delta>1 \<turnstile>\<^sub>T t : T \<Longrightarrow> k \<notin> fmv_trm t 0 \<Longrightarrow> (\<forall>x. x<k \<longrightarrow> \<Delta>1 x = \<Delta> x)
    \<Longrightarrow> (\<forall>x. x>k \<longrightarrow> \<Delta>1 x = \<Delta> (x-1)) \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm t k : T"
  "\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c \<Longrightarrow> k \<notin> fmv_cmd c 0 \<Longrightarrow> (\<forall>x. x<k \<longrightarrow> \<Delta>1 x = \<Delta> x)
    \<Longrightarrow> (\<forall>x. x>k \<longrightarrow> \<Delta>1 x = \<Delta> (x-1)) \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd c k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>T t : T; k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta>1 x = \<Delta> x; \<forall>x>k. \<Delta>1 x = \<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm t k : T) &&& (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c; k \<notin> fmv_cmd c 0; \<forall>x<k. \<Delta>1 x = \<Delta> x; \<forall>x>k. \<Delta>1 x = \<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd c k)
[PROOF STEP]
proof (induct arbitrary: k \<Delta> and k \<Delta> rule: typing_trm_typing_cmd.inducts)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> k \<Delta>'. \<lbrakk>\<Gamma> x = T; k \<notin> fmv_trm (`x) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (`x) k : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm s 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm s k : T1; k \<notin> fmv_trm (t \<degree> s) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (t \<degree> s) k : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 k \<Delta>'. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T2; k \<notin> fmv_trm (\<lambda>T1:t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (\<lambda>T1:t) k : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_cmd c 0; \<forall>x<k. (\<Delta>\<langle>0:T\<rangle>) x = \<Delta>' x; \<forall>x>k. (\<Delta>\<langle>0:T\<rangle>) x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>C dropM_cmd c k; k \<notin> fmv_trm (\<mu>T:c) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T
 5. \<And>\<Gamma> \<Delta> t T x k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T; \<Delta> x = T; k \<notin> fmv_cmd (<x>t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>C dropM_cmd (<x>t) k
[PROOF STEP]
case (activate \<Gamma> \<Delta> T c)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?k \<notin> fmv_cmd c 0; \<forall>x<?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> x; \<forall>x>?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta> \<turnstile>\<^sub>C dropM_cmd c ?k
k \<notin> fmv_trm (\<mu>T:c) 0
\<forall>x<k. \<Delta>'__ x = \<Delta> x
\<forall>x>k. \<Delta>'__ x = \<Delta> (x - 1)

goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> k \<Delta>'. \<lbrakk>\<Gamma> x = T; k \<notin> fmv_trm (`x) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (`x) k : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm s 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm s k : T1; k \<notin> fmv_trm (t \<degree> s) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (t \<degree> s) k : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 k \<Delta>'. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T2; k \<notin> fmv_trm (\<lambda>T1:t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (\<lambda>T1:t) k : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_cmd c 0; \<forall>x<k. (\<Delta>\<langle>0:T\<rangle>) x = \<Delta>' x; \<forall>x>k. (\<Delta>\<langle>0:T\<rangle>) x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>C dropM_cmd c k; k \<notin> fmv_trm (\<mu>T:c) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T
 5. \<And>\<Gamma> \<Delta> t T x k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T; \<Delta> x = T; k \<notin> fmv_cmd (<x>t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>C dropM_cmd (<x>t) k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?k \<notin> fmv_cmd c 0; \<forall>x<?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> x; \<forall>x>?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta> \<turnstile>\<^sub>C dropM_cmd c ?k
k \<notin> fmv_trm (\<mu>T:c) 0
\<forall>x<k. \<Delta>'__ x = \<Delta> x
\<forall>x>k. \<Delta>'__ x = \<Delta> (x - 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?k \<notin> fmv_cmd c 0; \<forall>x<?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> x; \<forall>x>?k. (\<Delta>'__\<langle>0:T\<rangle>) x = ?\<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta> \<turnstile>\<^sub>C dropM_cmd c ?k
k \<notin> fmv_trm (\<mu>T:c) 0
\<forall>x<k. \<Delta>'__ x = \<Delta> x
\<forall>x>k. \<Delta>'__ x = \<Delta> (x - 1)

goal (1 subgoal):
 1. \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T
[PROOF STEP]
apply(erule_tac x = "Suc k" in meta_allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; k \<notin> fmv_trm (\<mu>T:c) 0; \<forall>x<k. \<Delta>'__ x = \<Delta> x; \<forall>x>k. \<Delta>'__ x = \<Delta> (x - 1); \<And>\<Delta>. \<lbrakk>Suc k \<notin> fmv_cmd c 0; \<forall>x<Suc k. (\<Delta>'__\<langle>0:T\<rangle>) x = \<Delta> x; \<forall>x>Suc k. (\<Delta>'__\<langle>0:T\<rangle>) x = \<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd c (Suc k)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T
[PROOF STEP]
apply(insert fmv_suc(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; k \<notin> fmv_trm (\<mu>T:c) 0; \<forall>x<k. \<Delta>'__ x = \<Delta> x; \<forall>x>k. \<Delta>'__ x = \<Delta> (x - 1); \<And>\<Delta>. \<lbrakk>Suc k \<notin> fmv_cmd c 0; \<forall>x<Suc k. (\<Delta>'__\<langle>0:T\<rangle>) x = \<Delta> x; \<forall>x>Suc k. (\<Delta>'__\<langle>0:T\<rangle>) x = \<Delta> (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd c (Suc k); \<And>\<beta> c n. \<beta> \<notin> fmv_cmd c (Suc n) \<Longrightarrow> Suc \<beta> \<notin> fmv_cmd c n\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T
[PROOF STEP]
apply(clarsimp simp add: shift_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (\<mu>T:c) k : T

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> k \<Delta>'. \<lbrakk>\<Gamma> x = T; k \<notin> fmv_trm (`x) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (`x) k : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm s 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm s k : T1; k \<notin> fmv_trm (t \<degree> s) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (t \<degree> s) k : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 k \<Delta>'. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T2; k \<notin> fmv_trm (\<lambda>T1:t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm (\<lambda>T1:t) k : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> t T x k \<Delta>'. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>k \<Delta>'. \<lbrakk>k \<notin> fmv_trm t 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>T dropM_trm t k : T; \<Delta> x = T; k \<notin> fmv_cmd (<x>t) 0; \<forall>x<k. \<Delta> x = \<Delta>' x; \<forall>x>k. \<Delta> x = \<Delta>' (x - 1)\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>' \<turnstile>\<^sub>C dropM_cmd (<x>t) k
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma liftL_ctxt_type:
  assumes "\<Gamma>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : T \<Leftarrow> U"
  shows   "\<forall>k. \<Gamma>\<langle>k:T1\<rangle>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t (liftL_ctxt E k) : T \<Leftarrow> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<Gamma>\<langle>k:T1\<rangle> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t liftL_ctxt E k : T \<Leftarrow> U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : T \<Leftarrow> U

goal (1 subgoal):
 1. \<forall>k. \<Gamma>\<langle>k:T1\<rangle> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t liftL_ctxt E k : T \<Leftarrow> U
[PROOF STEP]
by (induct rule: typing_ctxt.induct) (auto simp add: liftL_type)


[STATEMENT]
lemma liftM_ctxt_type:
  assumes "\<Gamma>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : T \<Leftarrow> U"
  shows   "\<Gamma>, \<Delta>\<langle>k:T1\<rangle> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t (liftM_ctxt E k) : T \<Leftarrow> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>k:T1\<rangle> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t liftM_ctxt E k : T \<Leftarrow> U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : T \<Leftarrow> U

goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>k:T1\<rangle> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t liftM_ctxt E k : T \<Leftarrow> U
[PROOF STEP]
by(induct rule: typing_ctxt.induct) (auto simp add: liftM_type)


[STATEMENT]
theorem subst_type:
  "\<Gamma>1, \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>T r : T1 \<Longrightarrow> \<Gamma>1 = \<Gamma>\<langle>k:T1\<rangle> \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T"
  "\<Gamma>1, \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>T r : T1 \<Longrightarrow> \<Gamma>1 = \<Gamma>\<langle>k:T1\<rangle> \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>C c[r/k]\<^sup>C "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Gamma>1 , \<Delta> \<turnstile>\<^sub>T t : T; \<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma>1 = \<Gamma>\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T) &&& (\<lbrakk>\<Gamma>1 , \<Delta> \<turnstile>\<^sub>C c; \<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma>1 = \<Gamma>\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C c[r/k]\<^sup>C)
[PROOF STEP]
proof(induct arbitrary: \<Gamma> k T1 r and \<Gamma> k r T1 rule: typing_trm_typing_cmd.inducts)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 \<Gamma>' k T1a r. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma>\<langle>0:T1\<rangle> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T2; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<lambda>T1:t)[r/k]\<^sup>T : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c \<Gamma>' k T1 r. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Gamma>' k r T1. \<lbrakk>\<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[r/k]\<^sup>C; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
 5. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
case (lambda \<Gamma> T1 \<Delta> t T2)
[PROOF STATE]
proof (state)
this:
\<Gamma>'__\<langle>0:T1a__\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2
\<lbrakk>?\<Gamma> , \<Delta> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__\<langle>0:T1a__\<rangle> = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta> \<turnstile>\<^sub>T t[?r/?k]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>

goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 \<Gamma>' k T1a r. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma>\<langle>0:T1\<rangle> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T2; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<lambda>T1:t)[r/k]\<^sup>T : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c \<Gamma>' k T1 r. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Gamma>' k r T1. \<lbrakk>\<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[r/k]\<^sup>C; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
 5. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>'__\<langle>0:T1a__\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2
\<lbrakk>?\<Gamma> , \<Delta> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__\<langle>0:T1a__\<rangle> = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta> \<turnstile>\<^sub>T t[?r/?k]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>'__\<langle>0:T1a__\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2
\<lbrakk>?\<Gamma> , \<Delta> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__\<langle>0:T1a__\<rangle> = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta> \<turnstile>\<^sub>T t[?r/?k]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>

goal (1 subgoal):
 1. \<Gamma> , \<Delta> \<turnstile>\<^sub>T (\<lambda>T1a__:t)[r/k]\<^sup>T : T1a__ \<rightarrow> T2
[PROOF STEP]
by -(rotate_tac 2, drule liftL_type(1), fastforce)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T (\<lambda>T1a__:t)[r/k]\<^sup>T : T1a__ \<rightarrow> T2

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Gamma>' k T1 r. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Gamma>' k r T1. \<lbrakk>\<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[r/k]\<^sup>C; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Gamma>' k T1 r. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Gamma>' k r T1. \<lbrakk>\<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[r/k]\<^sup>C; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
case (activate \<Gamma> \<Delta> T c)
[PROOF STATE]
proof (state)
this:
\<Gamma>'__ , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__ = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[?r/?k]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Gamma>' k T1 r. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Gamma>' k r T1. \<lbrakk>\<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[r/k]\<^sup>C; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>'__ , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__ = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[?r/?k]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>'__ , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>T ?r : ?T1.0; \<Gamma>'__ = ?\<Gamma>\<langle>?k:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c[?r/?k]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>T r : T1
\<Gamma>'__ = \<Gamma>\<langle>k:T1\<rangle>

goal (1 subgoal):
 1. \<Gamma> , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T
[PROOF STEP]
by -(rotate_tac 2, drule liftM_type(1), fastforce)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T (\<mu>T:c)[r/k]\<^sup>T : T

goal (3 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Gamma>' k T1 r. \<lbrakk>\<Gamma> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (`x)[r/k]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Gamma>' k T1a r. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Gamma>' k T1a r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T s[r/k]\<^sup>T : T1; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1a; \<Gamma> = \<Gamma>'\<langle>k:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T (t \<degree> s)[r/k]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> t T x \<Gamma>' k r T1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Gamma>' k T1 r. \<lbrakk>\<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>T t[r/k]\<^sup>T : T; \<Delta> x = T; \<Gamma>' , \<Delta> \<turnstile>\<^sub>T r : T1; \<Gamma> = \<Gamma>'\<langle>k:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>' , \<Delta> \<turnstile>\<^sub>C (<x>t)[r/k]\<^sup>C
[PROOF STEP]
qed force+


[STATEMENT]
lemma struct_subst_command:
  assumes "\<Gamma>, \<Delta> \<turnstile>\<^sub>T t : T" "\<Delta> x = T" "\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1" "\<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>"
          "(\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1 \<Longrightarrow> \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> (liftM_ctxt E \<beta>)]\<^sup>T : T)"
  shows   "\<Gamma>,( \<Delta>'\<langle>\<beta>:U\<rangle>) \<turnstile>\<^sub>C (<x> t)[\<alpha>=\<beta> (liftM_ctxt E \<beta>)]\<^sup>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T
\<Delta> x = T
\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>
\<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T

goal (1 subgoal):
 1. \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>'\<langle>\<alpha>:T1\<rangle> \<turnstile>\<^sub>T t : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>; \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; T = (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x\<rbrakk> \<Longrightarrow> (\<beta> \<le> x \<and> x < \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <Suc x>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T) \<and> ((\<beta> \<le> x \<longrightarrow> \<not> x < \<alpha>) \<longrightarrow> (\<alpha> < x \<and> x \<le> \<beta> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <x - Suc 0>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T) \<and> ((\<alpha> < x \<longrightarrow> \<not> x \<le> \<beta>) \<longrightarrow> (x = \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <\<beta>>ctxt_subst (liftM_ctxt E \<beta>) (t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T)) \<and> (x \<noteq> \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <x>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T)))
[PROOF STEP]
apply (rule conjI, force, clarsimp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>'\<langle>\<alpha>:T1\<rangle> \<turnstile>\<^sub>T t : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>; \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; T = (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<beta> \<le> x \<longrightarrow> \<not> x < \<alpha>; \<alpha> < x \<longrightarrow> \<not> x \<le> \<beta>\<rbrakk> \<Longrightarrow> (x = \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <\<beta>>ctxt_subst (liftM_ctxt E \<beta>) (t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T)) \<and> (x \<noteq> \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <x>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> , \<Delta>'\<langle>\<alpha>:T1\<rangle> \<turnstile>\<^sub>T t : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>; \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; T = (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<beta> \<le> x \<longrightarrow> \<not> x < \<alpha>; \<alpha> < x \<longrightarrow> \<not> x \<le> \<beta>\<rbrakk> \<Longrightarrow> x = \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <\<beta>>ctxt_subst (liftM_ctxt E \<beta>) (t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T)
 2. \<lbrakk>\<Gamma> , \<Delta>'\<langle>\<alpha>:T1\<rangle> \<turnstile>\<^sub>T t : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>; \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; T = (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<beta> \<le> x \<longrightarrow> \<not> x < \<alpha>; \<alpha> < x \<longrightarrow> \<not> x \<le> \<beta>\<rbrakk> \<Longrightarrow> x \<noteq> \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <x>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T
[PROOF STEP]
apply (metis liftM_ctxt_type passivate shift_eq typing_ctxt_correct2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>'\<langle>\<alpha>:T1\<rangle> \<turnstile>\<^sub>T t : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>; \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; T = (\<Delta>'\<langle>\<alpha>:T1\<rangle>) x; \<beta> \<le> x \<longrightarrow> \<not> x < \<alpha>; \<alpha> < x \<longrightarrow> \<not> x \<le> \<beta>\<rbrakk> \<Longrightarrow> x \<noteq> \<alpha> \<longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C <x>t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem struct_subst_type:
  "\<Gamma>, \<Delta>1 \<turnstile>\<^sub>T t : T \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1 \<Longrightarrow> \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle> \<Longrightarrow> \<Gamma>, \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> (liftM_ctxt E \<beta>)]\<^sup>T : T"
  "\<Gamma>, \<Delta>1 \<turnstile>\<^sub>C c \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1  \<Longrightarrow> \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle> \<Longrightarrow> \<Gamma>, \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> (liftM_ctxt E \<beta>)]\<^sup>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>T t : T; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T) &&& (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C)
[PROOF STEP]
proof (induct arbitrary: \<Delta> T1 E U \<beta> \<alpha> and \<Delta> T1 E U \<beta> \<alpha> rule: typing_trm_typing_cmd.inducts)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<lambda>T1:t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>\<langle>0:T\<rangle> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 5. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
case (lambda \<Gamma> T1 \<Delta> t T2)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<langle>0:T1a__\<rangle> , \<Delta>'__ \<turnstile>\<^sub>T t : T2
\<lbrakk>\<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<lambda>T1:t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>\<langle>0:T\<rangle> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 5. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<langle>0:T1a__\<rangle> , \<Delta>'__ \<turnstile>\<^sub>T t : T2
\<lbrakk>\<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<langle>0:T1a__\<rangle> , \<Delta>'__ \<turnstile>\<^sub>T t : T2
\<lbrakk>\<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma>\<langle>0:T1a__\<rangle> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<lambda>T1a__:t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1a__ \<rightarrow> T2
[PROOF STEP]
by -(drule liftL_ctxt_type, fastforce simp: liftLM_comm_ctxt)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<lambda>T1a__:t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1a__ \<rightarrow> T2

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>\<langle>0:T\<rangle> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>\<langle>0:T\<rangle> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
case (activate \<Gamma> \<Delta> T c)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__\<langle>0:T\<rangle> = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>C c[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> T c \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>\<langle>0:T\<rangle> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 4. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__\<langle>0:T\<rangle> = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>C c[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta>'__\<langle>0:T\<rangle> \<turnstile>\<^sub>C c
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__\<langle>0:T\<rangle> = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>C c[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>C
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
[PROOF STEP]
by -(drule liftM_ctxt_type, fastforce simp: liftMM_comm_ctxt)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (\<mu>T:c)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T

goal (3 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
case (passivate \<Gamma> \<Delta> t T x)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>'__ \<turnstile>\<^sub>T t : T
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T
\<Delta>'__ x = T
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (3 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
 3. \<And>\<Gamma> \<Delta> t T x \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>\<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T; \<Delta> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> , \<Delta>'__ \<turnstile>\<^sub>T t : T
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T
\<Delta>'__ x = T
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta>'__ \<turnstile>\<^sub>T t : T
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T
\<Delta>'__ x = T
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>

goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
using struct_subst_command
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta>'__ \<turnstile>\<^sub>T t : T
\<lbrakk>\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; \<Delta>'__ = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : T
\<Delta>'__ x = T
\<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
\<Delta>'__ = \<Delta>\<langle>\<alpha>:T1\<rangle>
\<lbrakk>?\<Gamma> , ?\<Delta> \<turnstile>\<^sub>T ?t : ?T; ?\<Delta> ?x = ?T; ?\<Gamma> , ?\<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; ?\<Delta> = ?\<Delta>'\<langle>?\<alpha>:?T1.0\<rangle>; \<lbrakk>?\<Gamma> , ?\<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; ?\<Delta> = ?\<Delta>'\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , ?\<Delta>'\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T ?t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : ?T\<rbrakk> \<Longrightarrow> ?\<Gamma> , ?\<Delta>'\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>C (<?x>?t)[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>C

goal (1 subgoal):
 1. \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C (<x>t)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C

goal (2 subgoals):
 1. \<And>\<Gamma> x T \<Delta> \<Delta>' T1 E U \<beta> \<alpha>. \<lbrakk>\<Gamma> x = T; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta> = \<Delta>'\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (`x)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s \<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T t[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>\<Delta>' T1a E U \<beta> \<alpha>. \<lbrakk>\<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T s[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T1; \<Gamma> , \<Delta>' \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1a; \<Delta> = \<Delta>'\<langle>\<alpha>:T1a\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>'\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>T (t \<degree> s)[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>T : T2
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma struct_subst_type_command:  "\<Gamma>, \<Delta>1 \<turnstile>\<^sub>C c \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1
    \<Longrightarrow> \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle>
    \<Longrightarrow> \<Gamma>, \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> (liftM_ctxt E \<beta>)]\<^sup>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
using struct_subst_type
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> , ?\<Delta>1.0 \<turnstile>\<^sub>T ?t : ?T; ?\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; ?\<Delta>1.0 = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>T ?t[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>T : ?T
\<lbrakk>?\<Gamma> , ?\<Delta>1.0 \<turnstile>\<^sub>C ?c; ?\<Gamma> , ?\<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E : ?U \<Leftarrow> ?T1.0; ?\<Delta>1.0 = ?\<Delta>\<langle>?\<alpha>:?T1.0\<rangle>\<rbrakk> \<Longrightarrow> ?\<Gamma> , ?\<Delta>\<langle>?\<beta>:?U\<rangle> \<turnstile>\<^sub>C ?c[?\<alpha>=?\<beta> liftM_ctxt ?E ?\<beta>]\<^sup>C

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t E : U \<Leftarrow> T1; \<Delta>1 = \<Delta>\<langle>\<alpha>:T1\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>\<beta>:U\<rangle> \<turnstile>\<^sub>C c[\<alpha>=\<beta> liftM_ctxt E \<beta>]\<^sup>C
[PROOF STEP]
by force


[STATEMENT]
lemma dropM_env:
  "\<Gamma>, \<Delta>1 \<turnstile>\<^sub>T t[k=x \<diamond>]\<^sup>T : T \<Longrightarrow> \<Delta>1 = \<Delta>\<langle>x:(\<Delta> x)\<rangle> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (t[k=x \<diamond>]\<^sup>T) x : T"
  "\<Gamma>, \<Delta>1 \<turnstile>\<^sub>C c[k=x \<diamond>]\<^sup>C \<Longrightarrow> \<Delta>1 = \<Delta>\<langle>x:(\<Delta> x)\<rangle> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd (c[k=x \<diamond>]\<^sup>C) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>T t[k=x \<diamond>]\<^sup>T : T; \<Delta>1 = \<Delta>\<langle>x:\<Delta> x\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T dropM_trm (t[k=x \<diamond>]\<^sup>T) x : T) &&& (\<lbrakk>\<Gamma> , \<Delta>1 \<turnstile>\<^sub>C c[k=x \<diamond>]\<^sup>C; \<Delta>1 = \<Delta>\<langle>x:\<Delta> x\<rangle>\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd (c[k=x \<diamond>]\<^sup>C) x)
[PROOF STEP]
by (induct t and c arbitrary: \<Gamma> T \<Delta>1 x k \<Delta> and \<Gamma> T \<Delta>1 x k \<Delta>) fastforce+