diff --git a/Defs.thy b/Defs.thy
index 64e5533..eaadfae 100644
--- a/Defs.thy
+++ b/Defs.thy
@@ -27,6 +27,13 @@ proof goal_cases
 qed (auto simp: eqvt_def isin_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
+nominal_function set_alts :: "alt_list \<Rightarrow> alt fset" where
+  "set_alts ANil = {||}"
+| "set_alts (ACons alt alts) = finsert alt (set_alts alts)"
+       apply (auto simp: eqvt_def set_alts_graph_aux_def)
+  by (cases rule: term_alt_list_alt.exhaust(2)) auto
+nominal_termination (eqvt) by lexicographic_order
+
 nominal_function head_ctor :: "term \<Rightarrow> bool" where
   "head_ctor (Var _) = False"
 | "head_ctor (Lam _ _ _) = False"
@@ -35,34 +42,59 @@ nominal_function head_ctor :: "term \<Rightarrow> bool" where
 | "head_ctor (TApp e _) = head_ctor e"
 | "head_ctor (Ctor _) = True"
 | "head_ctor (Let _ _ _ _) = False"
+| "head_ctor (Case _ _) = False"
 proof goal_cases
   case (3 P x)
-  then show ?case by (cases x rule: term.exhaust)
+  then show ?case by (cases x rule: term_alt_list_alt.exhaust(1))
 qed (auto simp: eqvt_def head_ctor_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
+nominal_function head_data :: "\<tau> \<Rightarrow> (data_name * \<tau> list) option" where
+  "head_data (TyVar _) = None"
+| "head_data (TyData T) = Some (T, [])"
+| "head_data TyArrow = None"
+| "head_data (TyApp \<tau>1 \<tau>2) = (case head_data \<tau>1 of
+    Some (T, xs) \<Rightarrow> Some (T, xs @ [\<tau>2])
+  | None \<Rightarrow> None)"
+| "head_data (TyForall _ _ _) = None"
+proof goal_cases
+  case (3 P x)
+  then show ?case
+  proof (cases x rule: \<tau>.exhaust)
+    case (TyApp \<tau>1 \<tau>2)
+    then show ?thesis using 3 by (cases \<tau>1 rule: \<tau>.exhaust) auto
+  qed
+qed (auto simp: eqvt_def head_data_graph_aux_def split!: option.splits)
+nominal_termination (eqvt) by lexicographic_order
+
+nominal_function set_alt_list :: "alt_list \<Rightarrow> alt set" where
+  "set_alt_list ANil = {}"
+| "set_alt_list (ACons alt alts) = insert alt (set_alt_list alts)"
+proof goal_cases
+  case (3 P x)
+  then show ?case by (cases x rule: term_alt_list_alt.exhaust(2))
+qed (auto simp: eqvt_def set_alt_list_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
 nominal_function ctor_data_app :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
   "ctor_data_app (TyVar _) = None"
 | "ctor_data_app (TyData T) = Some (T, [])"
 | "ctor_data_app TyArrow = None"
 | "ctor_data_app (TyApp \<tau>1 (TyVar a)) = (case ctor_data_app \<tau>1 of
-    Some (T, s) \<Rightarrow> Some (T, a#s)
+    Some (T, tys) \<Rightarrow> Some (T, a#tys)
   | None \<Rightarrow> None)"
-| "ctor_data_app (TyApp _ (TyData _)) = None"
-| "ctor_data_app (TyApp _ TyArrow) = None"
-| "ctor_data_app (TyApp _ (TyApp _ _)) = None"
-| "ctor_data_app (TyApp _ (TyForall _ _ _)) = None"
+| "\<nexists>a. \<tau>2 = TyVar a \<Longrightarrow> ctor_data_app (TyApp _ \<tau>2) = None"
 | "ctor_data_app (TyForall _ _ _) = None"
 proof goal_cases
-  case 1
+case 1
   then show ?case by (auto simp: eqvt_def ctor_data_app_graph_aux_def split!: option.splits)
 next
   case (3 P x)
   then show ?case
   proof (cases x rule: \<tau>.exhaust)
     case (TyApp \<tau>1 \<tau>2)
-    then show ?thesis using 3 by (cases \<tau>2 rule: \<tau>.exhaust) auto
-  qed (auto simp: 3)
+    then show ?thesis using 3 by (cases "\<exists>a. \<tau>2 = TyVar a") auto
+  qed auto
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
@@ -71,49 +103,32 @@ nominal_function ctor_type_app :: "\<tau> \<Rightarrow> (data_name * tyvar list)
 | "ctor_type_app (TyData T) = Some (T, [])"
 | "ctor_type_app TyArrow = None"
 | "ctor_type_app (TyApp (TyApp TyArrow \<tau>1) \<tau>2) = ctor_type_app \<tau>2"
-| "ctor_type_app (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2)"
-| "ctor_type_app (TyApp (TyApp (TyData T) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyData T) \<tau>1) \<tau>2)"
-| "ctor_type_app (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2)"
-| "ctor_type_app (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2)"
-| "ctor_type_app (TyApp (TyVar a) \<tau>2) = ctor_data_app (TyApp (TyVar a) \<tau>2)"
-| "ctor_type_app (TyApp (TyData T) \<tau>2) = ctor_data_app (TyApp (TyData T) \<tau>2)"
-| "ctor_type_app (TyApp TyArrow \<tau>2) = ctor_data_app (TyApp TyArrow \<tau>2)"
-| "ctor_type_app (TyApp (TyForall a k e) \<tau>2) = ctor_data_app (TyApp (TyForall a k e) \<tau>2)"
+| "\<nexists>\<tau>1'. \<tau>1 = TyApp TyArrow \<tau>1' \<Longrightarrow> ctor_type_app (TyApp \<tau>1 \<tau>2) = ctor_data_app (TyApp \<tau>1 \<tau>2)"
 | "ctor_type_app (TyForall _ _ _) = None"
 proof goal_cases
   case (3 P x)
-  show ?case using 3(1-3,13)
+  then show ?case
   proof (cases x rule: \<tau>.exhaust)
-    case outer: (TyApp \<tau>1 \<tau>2)
-    then show ?thesis using 3(9-12)
-    proof (cases \<tau>1 rule: \<tau>.exhaust)
-      case inner: (TyApp \<tau>1' \<tau>2')
-      then show ?thesis using outer 3(4-8) by (cases \<tau>1' rule: \<tau>.exhaust) blast+
-    qed blast+
-  qed blast+
-next
-  case (74 a k e \<tau>1 \<tau>2 a k e \<tau>1 \<tau>2)
-  then show ?case by (simp add: 74)
-next
-  case (92 a k e \<tau>2 a k e \<tau>2)
-  then show ?case by (simp add: 92)
+    case (TyApp e1 e2)
+    then show ?thesis using 3(4,5) by (cases "\<nexists>\<tau>1'. e1 = TyApp TyArrow \<tau>1'") auto
+  qed (auto simp: 3)
 qed (auto simp: eqvt_def ctor_type_app_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function ctor_type_forall :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
+nominal_function ctor_type_forall :: "\<tau> \<Rightarrow> (data_name * tyvar list * \<kappa> list) option" where
   "ctor_type_forall (TyVar _) = None"
-| "ctor_type_forall (TyData T) = Some (T, [])"
+| "ctor_type_forall (TyData T) = Some (T, [], [])"
 | "ctor_type_forall TyArrow = None"
-| "ctor_type_forall (TyApp \<tau>1 \<tau>2) = ctor_type_app (TyApp \<tau>1 \<tau>2)"
-| "ctor_type_forall (TyForall a _ e) = (case ctor_type_forall e of
-    Some (T, s) \<Rightarrow> (if a \<in> set s then Some (T, filter (\<lambda>x. x \<noteq> a) s) else None)
-  | None \<Rightarrow> None)"
+| "ctor_type_forall (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, tys) \<Rightarrow> Some (T, tys, []) | None \<Rightarrow> None)"
+| "ctor_type_forall (TyForall a k e) = (case ctor_type_forall e of
+    Some (T, xs, ks) \<Rightarrow> (if a \<in> set xs then Some (T, filter (\<lambda>x. x \<noteq> a) xs, k#ks) else None)
+  | _ \<Rightarrow> None)"
 proof goal_cases
   case 1
   then show ?case by (auto simp: eqvt_def ctor_type_forall_graph_aux_def split!: option.splits list.splits)
 next
   case (3 P x)
-  then show ?case by (cases x rule: \<tau>.exhaust)
+  then show ?case by (cases x rule: \<tau>.exhaust) auto
 next
   case (18 a k e a' k' e')
   obtain c::tyvar where P: "atom c \<sharp> (a, e, a', e', ctor_type_forall_sumC e, ctor_type_forall_sumC e')" by (rule obtain_fresh)
@@ -124,9 +139,10 @@ next
   then show ?case
   proof (cases "ctor_type_forall_sumC e")
     case (Some t)
-    then obtain T s where P1: "t = (T, s)" by fastforce
-    from Some obtain T' s' where P2: "ctor_type_forall_sumC e' = Some (T', s')" using 3 by auto
-    have "T = T'" using "2" P1 P2 Some Some_eqvt option.inject perm_data_name_tyvar by auto
+    then obtain T s ks where P1: "t = (T, s, ks)" by (metis prod.exhaust)
+    from Some obtain T' s' ks' where P2: "ctor_type_forall_sumC e' = Some (T', s', ks')" using 3 by auto
+    then have pairs: "(a \<leftrightarrow> c) \<bullet> (T, s, ks) = (a' \<leftrightarrow> c) \<bullet> (T', s', ks')" using 2 P1 Some Some_eqvt option.inject by simp
+    from pairs have "T = T'" "ks = ks'" by auto
     have same: "(a \<leftrightarrow> c) \<bullet> s = (a' \<leftrightarrow> c) \<bullet> s'" using "2" P1 P2 Some by auto
     have x: "a \<in> set s \<longleftrightarrow> a' \<in> set s'" by (metis flip_at_simps(2) mem_permute_iff permute_flip_cancel same set_eqvt)
     have 4: "atom c \<sharp> s" using c(5) Some P1 fresh_Some fresh_Pair by metis
@@ -137,19 +153,26 @@ next
     also have "... = filter (\<lambda>x. x \<noteq> c) ((a' \<leftrightarrow> c) \<bullet> s')" using same by argo
     also have "... = (a' \<leftrightarrow> c) \<bullet> filter (\<lambda>x. x \<noteq> a') s'" by simp
     also have "... = filter (\<lambda>x. x \<noteq> a') s'" using 6 flip_fresh_fresh by blast
-    finally have 9: "Some (T, filter (\<lambda>x. x \<noteq> a) s) = Some (T', filter (\<lambda>x. x \<noteq> a') s')" using \<open>T = T'\<close> by blast
-    then show ?thesis using Some P1 P2 x by simp
+    finally have 9: "Some (T, filter (\<lambda>x. x \<noteq> a) s, ks) = Some (T', filter (\<lambda>x. x \<noteq> a') s', ks')" using \<open>T = T'\<close> \<open>ks = ks'\<close> by blast
+    then show ?thesis
+    proof (cases "a \<in> set s")
+      case True
+      then show ?thesis using Some P1 P2 x 18(5) 9 by simp
+    next
+      case False
+      then show ?thesis using P1 P2 Some x by force
+    qed  
   qed simp
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
 (* This function checks if a type has the form \<forall>[a:k]. [\<tau>] \<rightarrow> T [a] *)
-nominal_function ctor_type :: "\<tau> \<Rightarrow> data_name option" where
+nominal_function ctor_type :: "\<tau> \<Rightarrow> (data_name * \<kappa> list) option" where
   "ctor_type (TyVar a) = None"
-| "ctor_type (TyData T) = Some T"
+| "ctor_type (TyData T) = Some (T, [])"
 | "ctor_type TyArrow = None"
-| "ctor_type (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
-| "ctor_type (TyForall a k e) = (case ctor_type_forall (TyForall a k e) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
+| "ctor_type (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, []) \<Rightarrow> Some (T, []) | _ \<Rightarrow> None)"
+| "ctor_type (TyForall a k e) = (case ctor_type_forall (TyForall a k e) of Some (T, [], ks) \<Rightarrow> Some (T, ks) | _ \<Rightarrow> None)"
 proof goal_cases
   case 1
   then show ?case by (auto simp: eqvt_def ctor_type_graph_aux_def split!: option.splits list.splits)
@@ -158,10 +181,34 @@ next
   then show ?case by (cases x rule: \<tau>.exhaust)
 next
   case (18 a k e a' k' e')
-  then show ?case by (simp add: 18)
+  have "(case ctor_type_forall (\<forall> a' : k' . e') of None \<Rightarrow> None | Some (d, [], ks) \<Rightarrow> Some (d, k # ks) | Some (d, t # x, ks) \<Rightarrow> Map.empty x) = (case ctor_type_forall (\<forall> a' : k' . e') of None \<Rightarrow> None | Some (d, [], ks) \<Rightarrow> Some (d, k' # ks) | Some (d, t # x, ks) \<Rightarrow> Map.empty x)"
+    using "18" by fastforce
+  then show ?case
+    by (simp add: "18")
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
+abbreviation exhaustive :: "alt_list \<Rightarrow> \<Delta> \<Rightarrow> data_name \<Rightarrow> bool" where
+  "exhaustive alts \<Delta> T \<equiv> \<forall>D \<tau> ks. (AxCtor D \<tau> \<in> set \<Delta> \<and> ctor_type \<tau> = Some (T, ks)) \<longrightarrow> (\<exists>tys vals e. MatchCtor D tys vals e |\<in>| set_alts alts)"
+
+nominal_function zip_with :: "('a::pt \<Rightarrow> 'b::pt \<Rightarrow> 'c::pt) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+  "zip_with _ [] _ = []"
+| "zip_with _ _ [] = []"
+| "zip_with f (a#as) (b#bs) = f a b # zip_with f as bs"
+proof goal_cases
+  case (3 P x)
+  then obtain f xs ys where P: "x = (f, xs, ys)" by (metis prod.exhaust)
+  then show ?case using 3
+  proof (cases xs)
+    case (Cons a list)
+    then show ?thesis using 3 P by (cases ys) auto
+  qed simp
+qed (auto simp: eqvt_def zip_with_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
+lemma zip_with_length[simp]: "length (zip_with f as bs) = min (length as) (length bs)"
+  by (induction f as bs rule: zip_with.induct) auto
+
 nominal_function is_value :: "term => bool" where
   "is_value (Var x) = False"
 | "is_value (\<lambda> x : \<tau> . e) = True"
@@ -170,44 +217,105 @@ nominal_function is_value :: "term => bool" where
 | "is_value (TApp e \<tau>) = head_ctor e"
 | "is_value (Ctor _) = True"
 | "is_value (Let x \<tau> e1 e2) = False"
+| "is_value (Case _ _) = False"
 proof goal_cases
   case (3 P x)
-  then show ?case by (cases x rule: term.exhaust)
+  then show ?case by (cases x rule: term_alt_list_alt.exhaust(1))
 next
-  case (17 a k e a' k' e')
+  case (19 a k e a' k' e')
   obtain c::tyvar where c: "atom c \<sharp> (a, e, a', e')" by (rule obtain_fresh)
   have 1: "is_value_sumC e' = (a' \<leftrightarrow> c) \<bullet> is_value_sumC e'" using permute_boolE permute_boolI by blast
   have 2: "is_value_sumC e = (a \<leftrightarrow> c) \<bullet> is_value_sumC e" using permute_boolE permute_boolI by blast
-  from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 17(5) by simp
-  then show ?case using 1 2 17(1,2) eqvt_at_def by metis
+  from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 19(5) by simp
+  then show ?case using 1 2 19(1,2) eqvt_at_def by metis
 qed (auto simp: eqvt_def is_value_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_term :: "term => term \<Rightarrow> var => term" where
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+  subst_term :: "term => term \<Rightarrow> var => term" and
+  subst_alt_list :: "alt_list \<Rightarrow> term \<Rightarrow> var \<Rightarrow> alt_list" and
+  subst_alt :: "alt \<Rightarrow> term \<Rightarrow> var \<Rightarrow> alt" where
+
   "subst_term (Var y) e x  = (if x = y then e else Var y)"
 | "subst_term (App e1 e2) e x = App (subst_term e1 e x) (subst_term e2 e x)"
 | "subst_term (TApp e1 \<tau>) e x = TApp (subst_term e1 e x) \<tau>"
 | "subst_term (Ctor D) _ _ = Ctor D"
+| "subst_term (Case t alts) e x = Case (subst_term t e x) (subst_alt_list alts e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<lambda> y:\<tau>. e2) e x = (\<lambda> y:\<tau>. subst_term e2 e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<Lambda> y:k. e2) e x = (\<Lambda> y:k. subst_term e2 e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (Let y \<tau> e1 e2) e x = Let y \<tau> (subst_term e1 e x) (subst_term e2 e x)"
+
+| "subst_alt_list ANil _ _ = ANil"
+| "subst_alt_list (ACons alt alts) e x = ACons (subst_alt alt e x) (subst_alt_list alts e x)"
+
+| "set (map atom tys @ map atom vals) \<sharp>* (e, x) \<Longrightarrow> subst_alt (MatchCtor D tys vals t) e x = MatchCtor D tys vals (subst_term t e x)"
 proof (goal_cases)
-  case (3 P x)
-  then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
+
+  (* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
+  have eqvt_at_term: "\<And>e y z . eqvt_at subst_term_subst_alt_list_subst_alt_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term a b c) (e, y, z)"
+    apply (simp add: eqvt_at_def subst_term_def)
+    apply rule
+    apply (subst Projl_permute)
+     apply (simp add: subst_term_subst_alt_list_subst_alt_sumC_def)
+     apply (simp add: THE_default_def)
+     apply (case_tac "Ex1 (subst_term_subst_alt_list_subst_alt_graph (Inl (e, y, z)))")
+      apply(auto)[2]
+      apply (erule_tac x="x" in allE)
+      apply simp
+      apply(cases rule: subst_term_subst_alt_list_subst_alt_graph.cases)
+               apply(assumption)
+              apply blast+
+    apply simp
+    done
+
+{ case (3 P x)
   then show ?case
-    apply (cases t rule: term.strong_exhaust[of _ _ "(e, y)"])
-          apply (auto simp: 3)
-    using 3(5-7) P fresh_star_def by blast+
+  proof (cases x)
+    case (Inl a)
+    then obtain t e y where P: "a = (t, e, y)" by (metis prod.exhaust)
+    then show ?thesis using 3(1-5) Inl
+    proof (cases t rule: term_alt_list_alt.strong_exhaust(1)[of _ _ "(e, y)"])
+      case Lam
+      then show ?thesis using 3(6) Inl P fresh_star_insert by blast
+    next
+      case TyLam
+      then show ?thesis using 3(7) Inl P fresh_star_insert by blast
+    next
+      case Let
+      then show ?thesis using 3(8) Inl P fresh_star_insert by blast
+    qed auto
+  next
+    case outer: (Inr b)
+    then show ?thesis
+    proof (cases b)
+      case (Inl a)
+      then obtain xs e y where "a = (xs, e, y)" by (metis prod.exhaust)
+      then show ?thesis using 3(9,10) Inl outer by (cases xs rule: term_alt_list_alt.exhaust(2)) auto
+    next
+      case (Inr c)
+      then obtain m e y where "c = (m, e, y)" by (metis prod.exhaust)
+      then show ?thesis using 3 Inr outer fresh_star_insert
+        apply (cases m rule: term_alt_list_alt.strong_exhaust(3)[of "(e, y)"])
+        by auto
+    qed
+  qed
+next
+  case (49 y e x \<tau> e2 y' e' x' \<tau>' e2')
+  have "(\<lambda> y : \<tau> . subst_term e2 e x) = (\<lambda> y' : \<tau>' . subst_term e2' e' x')" using Abs_sumC[OF 49(5,6) eqvt_at_term[OF 49(1)] eqvt_at_term[OF 49(2)]] 49(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (26 y e x \<tau> e2 y' e' x' \<tau>' e2')
-  then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
+  case (55 y e x k e2 y' e' x' k' e2')
+  have "(\<Lambda> y : k . subst_term e2 e x) = (\<Lambda> y' : k' . subst_term e2' e' x')" using Abs_sumC[OF 55(5,6) eqvt_at_term[OF 55(1)] eqvt_at_term[OF 55(2)]] 55(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (29 y e x k e2 y' e' x' k' e2')
-  then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
+  case (60 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
+  have "Let y \<tau> (subst_term e1 e x) (subst_term e2 e x) = Let y' \<tau>' (subst_term e1' e' x') (subst_term e2' e' x')" using Abs_sumC[OF 60(9,10) eqvt_at_term[OF 60(2)] eqvt_at_term[OF 60(4)]] 60(11) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (31 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
-  then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
-qed (auto simp: eqvt_def subst_term_graph_aux_def)
+  case (69 tys vals e x D t tys' vals' e' x' D' t')
+  have "MatchCtor D tys vals (subst_term t e x) = MatchCtor D' tys' vals' (subst_term t' e' x')" using Abs_sumC_star[OF 69(5,6) eqvt_at_term[OF 69(1)] eqvt_at_term[OF 69(2)]] 69(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
+} qed (auto simp: eqvt_def subst_term_subst_alt_list_subst_alt_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" where
@@ -219,41 +327,101 @@ nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar
 proof goal_cases
   case (3 P x)
   then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
-  then show ?case
-    apply (cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
-       apply (auto simp: 3)
-    using 3(5) P fresh_star_def by blast
+  then show ?case proof(cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
+    case (TyForall x51 x52 x53)
+    then show ?thesis using 3(5) P fresh_star_def by blast
+  qed (auto simp: 3)
 next
   case (18 b \<tau> a k \<sigma> b' \<tau>' a' k' \<sigma>')
   then show ?case using Abs_sumC[OF 18(5,6,1,2)] by fastforce
 qed (auto simp: eqvt_def subst_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" where
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+  subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" and
+  subst_alt_list_type :: "alt_list \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> alt_list" and
+  subst_alt_type :: "alt \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> alt" where
+
   "subst_term_type (Var x) _ _ = Var x"
 | "subst_term_type (Ctor D) _ _ = Ctor D"
 | "subst_term_type (App e1 e2) \<tau> a = App (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
 | "subst_term_type (TApp e \<tau>2) \<tau> a = TApp (subst_term_type e \<tau> a) (subst_type \<tau>2 \<tau> a)"
+| "subst_term_type (Case e alts) \<tau> a = Case (subst_term_type e \<tau> a) (subst_alt_list_type alts \<tau> a)"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:(subst_type \<tau>' \<tau> a). subst_term_type e2 \<tau> a)"
 | "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. subst_term_type e2 \<tau> a)"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y (subst_type \<tau>' \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
+
+| "subst_alt_list_type ANil _ _ = ANil"
+| "subst_alt_list_type (ACons alt alts) \<tau> a = ACons (subst_alt_type alt \<tau> a) (subst_alt_list_type alts \<tau> a)"
+
+| "set (map atom tys @ map atom vals) \<sharp>* (\<tau>, a) \<Longrightarrow> subst_alt_type (MatchCtor D tys vals e) \<tau> a = MatchCtor D tys vals (subst_term_type e \<tau> a)"
 proof goal_cases
-  case (3 P x)
-  then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
+
+  (* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
+  have eqvt_at_term: "\<And>e y z . eqvt_at subst_term_type_subst_alt_list_type_subst_alt_type_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term_type a b c) (e, y, z)"
+    apply (simp add: eqvt_at_def subst_term_type_def)
+    apply rule
+    apply (subst Projl_permute)
+     apply (simp add: subst_term_type_subst_alt_list_type_subst_alt_type_sumC_def)
+     apply (simp add: THE_default_def)
+     apply (case_tac "Ex1 (subst_term_type_subst_alt_list_type_subst_alt_type_graph (Inl (e, y, z)))")
+      apply(auto)[2]
+      apply (erule_tac x="x" in allE)
+      apply simp
+      apply(cases rule: subst_term_type_subst_alt_list_type_subst_alt_type_graph.cases)
+               apply(assumption)
+              apply blast+
+    apply simp
+    done
+
+{ case (3 P x)
   then show ?case
-    apply (cases t rule: term.strong_exhaust[of _ _ "(\<tau>, a)"])
-    using 3 P apply auto[4]
-    using 3(5,6,7) P fresh_star_def by blast+
+  proof (cases x)
+    case (Inl a)
+    then obtain t e y where P: "a = (t, e, y)" by (metis prod.exhaust)
+    then show ?thesis using 3(1-5) Inl
+    proof (cases t rule: term_alt_list_alt.strong_exhaust(1)[of _ _ "(e, y)"])
+      case Lam
+      then show ?thesis using 3(6) Inl P fresh_star_insert by blast
+    next
+      case TyLam
+      then show ?thesis using 3(7) Inl P fresh_star_insert by blast
+    next
+      case Let
+      then show ?thesis using 3(8) Inl P fresh_star_insert by blast
+    qed auto
+  next
+    case outer: (Inr b)
+    then show ?thesis
+    proof (cases b)
+      case (Inl a)
+      then obtain xs e y where "a = (xs, e, y)" by (metis prod.exhaust)
+      then show ?thesis using 3(9,10) Inl outer by (cases xs rule: term_alt_list_alt.exhaust(2)) auto
+    next
+      case (Inr c)
+      then obtain m e y where P: "c = (m, e, y)" by (metis prod.exhaust)
+      then show ?thesis using Inr outer 3
+        apply (cases m rule: term_alt_list_alt.strong_exhaust(3)[of "(e, y)"]) by simp
+    qed
+  qed
 next
-  case (26 y \<tau> a \<tau>1 e2 y' \<tau>' a' \<tau>1' e2')
-  then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
+  case (49 y \<tau> a \<tau>2 e2 y' \<tau>' a' \<tau>2' e2')
+  have "(\<lambda> y : subst_type \<tau>2 \<tau> a . subst_term_type e2 \<tau> a) = (\<lambda> y' : subst_type \<tau>2' \<tau>' a' . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 49(5,6) eqvt_at_term[OF 49(1)] eqvt_at_term[OF 49(2)]] 49(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
 next
-  case (29 b \<tau> a k e2 b' \<tau>' a' k' e2')
-  then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
+  case (55 b \<tau> a k e2 b' \<tau>' a' k' e2')
+  have "(\<Lambda> b : k . subst_term_type e2 \<tau> a) = (\<Lambda> b' : k' . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 55(5,6) eqvt_at_term[OF 55(1)] eqvt_at_term[OF 55(2)]] 55(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
 next
-  case (31 y \<tau> a \<tau>1 e1 e2 y' \<tau>' a' \<tau>1' e1' e2')
-  then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
-qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
+  case (60 y \<tau> a \<tau>2 e1 e2 y' \<tau>' a' \<tau>2' e1' e2')
+  have "Let y (subst_type \<tau>2 \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a) = Let y' (subst_type \<tau>2' \<tau>' a') (subst_term_type e1' \<tau>' a') (subst_term_type e2' \<tau>' a')"
+    using Abs_sumC[OF 60(9,10) eqvt_at_term[OF 60(2)] eqvt_at_term[OF 60(4)]] 60(11) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
+next
+  case (69 tys vals \<tau> a D e tys' vals' \<tau>' a' D' e')
+  have "MatchCtor D tys vals (subst_term_type e \<tau> a) = MatchCtor D' tys' vals' (subst_term_type e' \<tau>' a')" using Abs_sumC_star[OF 69(5,6) eqvt_at_term[OF 69(1)] eqvt_at_term[OF 69(2)]] 69(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
+} qed (auto simp: eqvt_def subst_term_type_subst_alt_list_type_subst_alt_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" where
@@ -275,6 +443,37 @@ no_notation inverse_divide (infixl "'/" 70)
 consts subst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" ("_[_'/_]" [1000,0,0] 1000)
 
 adhoc_overloading
-  subst subst_term subst_type subst_term_type subst_context
+  subst subst_term subst_alt_list subst_alt subst_type subst_term_type subst_alt_list_type subst_alt_type subst_context
+
+fun get_tyvars :: "atom list \<Rightarrow> tyvar list" where
+  "get_tyvars [] = []"
+| "get_tyvars (a#as) = (if sort_of a = sort_of (atom (undefined :: tyvar))
+    then Abs_tyvar a # get_tyvars as
+    else get_tyvars as)"
+
+fun get_vars :: "atom list \<Rightarrow> var list" where
+  "get_vars [] = []"
+| "get_vars (a#as) = (if sort_of a = sort_of (atom (undefined :: var))
+    then Abs_var a # get_vars as
+    else get_vars as)"
+
+lemma get_tyvars_append: "get_tyvars (map atom (tys::tyvar list) @ map atom (vars::var list)) = tys"
+proof (induction tys arbitrary: vars)
+case Nil
+  then show ?case by (induction vars) auto
+next
+  case (Cons a tys)
+  then show ?case  apply auto by (simp add: Rep_tyvar_inverse atom_tyvar_def)
+qed
+
+lemma get_vars_append: "get_vars (map atom (tys::tyvar list) @ map atom (vars::var list)) = vars"
+proof (induction tys arbitrary: vars)
+  case outer: Nil
+  then show ?case
+  proof (induction vars)
+    case (Cons a vars)
+    then show ?case apply auto by (simp add: Rep_var_inverse atom_var_def)
+  qed simp
+qed simp
 
 end
diff --git a/Defs2.thy b/Defs2.thy
new file mode 100644
index 0000000..ebb2ef8
--- /dev/null
+++ b/Defs2.thy
@@ -0,0 +1,94 @@
+theory Defs2
+  imports Lemmas
+begin
+
+nominal_function ctor_data_app_subst :: "\<tau> \<Rightarrow> bool" where
+  "ctor_data_app_subst (TyVar _) = False"
+| "ctor_data_app_subst (TyData _) = True"
+| "ctor_data_app_subst TyArrow = False"
+| "ctor_data_app_subst (TyApp \<tau>1 _) = ctor_data_app_subst \<tau>1"
+| "ctor_data_app_subst (TyForall _ _ _) = False"
+proof goal_cases
+  case (3 P x)
+  then show ?case by (cases x rule: \<tau>.exhaust) auto
+qed (auto simp: eqvt_def ctor_data_app_subst_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
+nominal_function ctor_args :: "\<tau> \<Rightarrow> \<tau> list option" where
+  "ctor_args (TyVar _) = None"
+| "ctor_args (TyData T) = Some []"
+| "ctor_args TyArrow = None"
+| "ctor_args (TyApp (TyApp TyArrow \<tau>1) \<tau>2) = (case ctor_args \<tau>2 of
+    Some tys \<Rightarrow> Some (\<tau>1#tys)
+  | None \<Rightarrow> None)"
+| "\<nexists>\<tau>1'. \<tau>1 = TyApp TyArrow \<tau>1' \<Longrightarrow> ctor_args (TyApp \<tau>1 \<tau>2) = (if ctor_data_app_subst (TyApp \<tau>1 \<tau>2) then Some [] else None)"
+| "ctor_args (TyForall _ _ _) = None"
+proof goal_cases
+  case 1
+  then show ?case by (auto simp: eqvt_def ctor_args_graph_aux_def split!: option.splits)
+next
+  case (3 P x)
+  then show ?case
+  proof (cases x rule: \<tau>.exhaust)
+    case (TyApp \<tau>1 \<tau>2)
+    then show ?thesis using 3 by (cases "\<exists>\<tau>1'. \<tau>1 = TyApp TyArrow \<tau>1'") auto
+  qed auto
+qed auto
+nominal_termination (eqvt) by lexicographic_order
+
+nominal_function subst_ctor :: "\<tau> \<Rightarrow> \<tau> list \<Rightarrow> \<tau> list option" where
+  "subst_ctor (TyVar _) _ = None"
+| "subst_ctor TyArrow _ = None"
+| "subst_ctor (TyData _) [] = Some []"
+| "subst_ctor (TyData _) (_#_) = None"
+| "subst_ctor (TyApp \<tau>1 \<tau>2) [] = ctor_args (TyApp \<tau>1 \<tau>2)"
+| "subst_ctor (TyApp _ _) (_#_) = None"
+| "subst_ctor (TyForall _ _ _) [] = None"
+| "subst_ctor (TyForall a _ e) (\<tau>#\<tau>s) = subst_ctor e[\<tau>/a] \<tau>s"
+proof goal_cases
+  case (3 P x)
+  then obtain t xs where P: "x = (t, xs)" by fastforce
+  then show ?case using 3
+  proof (cases t rule: \<tau>.exhaust)
+    case TyData
+    then show ?thesis using P 3 by (cases xs) auto
+  next
+    case TyApp
+    then show ?thesis using P 3 by (cases xs) auto
+  next
+    case TyForall
+    then show ?thesis using P 3 by (cases xs) auto
+  qed auto
+next
+  case (39 a k e \<tau> \<tau>s a' k' e' \<tau>' \<tau>s')
+  then show ?case by (metis Pair_inject \<tau>.eq_iff(5) list.inject subst_same(2))
+qed (auto simp: eqvt_def subst_ctor_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
+lemma supp_ctor_args: "ctor_args \<tau> = Some args \<Longrightarrow> supp args \<subseteq> supp \<tau>"
+proof (induction \<tau> arbitrary: args rule: ctor_args.induct)
+  case (2 T)
+  then show ?case unfolding \<tau>.supp(2) pure_supp using supp_Nil by simp
+next
+  case (4 \<tau>1 \<tau>2)
+  then show ?case apply (auto split!: option.splits) unfolding \<tau>.supp supp_Cons by auto
+next
+  case (5 \<tau>1 \<tau>2 a)
+  then show ?case using supp_Nil by (auto split!: if_splits)
+qed auto
+
+lemma supp_subst_ctor: "subst_ctor \<tau> \<tau>s = Some args \<Longrightarrow> supp args \<subseteq> supp \<tau> \<union> supp \<tau>s"
+proof (induction \<tau> \<tau>s arbitrary: args rule: subst_ctor.induct)
+  case (3 T)
+  then show ?case unfolding \<tau>.supp(2) pure_supp by simp
+next
+  case (5 \<tau>1 \<tau>2)
+  then have "ctor_args (TyApp \<tau>1 \<tau>2) = Some args" by simp
+  then show ?case using supp_Nil supp_ctor_args by auto
+next
+  case (8 a k e \<tau> \<tau>s)
+  then have "supp args \<subseteq> supp e[\<tau>/a] \<union> supp \<tau>s" by simp
+  then show ?case unfolding \<tau>.supp(5) pure_supp supp_Cons using supp_subst_type by fastforce
+qed auto
+
+end
\ No newline at end of file
diff --git a/Lemmas.thy b/Lemmas.thy
index b520a3a..7622018 100644
--- a/Lemmas.thy
+++ b/Lemmas.thy
@@ -2,31 +2,104 @@ theory Lemmas
   imports Syntax Defs
 begin
 
+lemma fresh_match_Pair:
+  fixes tys::"tyvar list" and vals::"var list"
+  assumes "set (map atom tys) \<sharp>* e" "set (map atom vals) \<sharp>* e" "set (map atom tys) \<sharp>* y"  "set (map atom vals) \<sharp>* y"
+  shows "set (map atom tys @ map atom vals) \<sharp>* (e, y)"
+  by (metis assms fresh_star_Pair fresh_star_Un set_append)
+
+lemma fresh_in_match_var:
+  fixes x::"var"
+  assumes "set (map atom tys) \<sharp>* x" "set (map atom vals) \<sharp>* x" "atom x \<sharp> MatchCtor D tys vals e"
+  shows "atom x \<sharp> e"
+  using assms fresh_at_base(2) fresh_star_Un fresh_star_def by fastforce
+
+lemma fresh_in_match_tyvar:
+  fixes a::"tyvar"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "atom a \<sharp> MatchCtor D tys vals e"
+  shows "atom a \<sharp> e"
+  using assms fresh_at_base(2) fresh_star_Un fresh_star_def by fastforce
+lemmas fresh_in_match = fresh_in_match_var fresh_in_match_tyvar
+
+lemma fresh_star_invert: "set (map atom xs) \<sharp>* a \<Longrightarrow> atom a \<sharp> xs"
+  unfolding fresh_star_def by (induction xs) (auto simp: fresh_Cons fresh_Nil fresh_at_base(2))
+
+lemma match_ctor_eqvt_var:
+  fixes a c::"var"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "set (map atom tys) \<sharp>* c" "set (map atom vals) \<sharp>* c"
+  shows "(a \<leftrightarrow> c) \<bullet> MatchCtor D tys vals e = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)"
+proof -
+  from assms(1,3) have 1: "(a \<leftrightarrow> c) \<bullet> tys = tys" using fresh_star_invert flip_fresh_fresh by blast
+  from assms(2,4) have 2: "(a \<leftrightarrow> c) \<bullet> vals = vals" using fresh_star_invert flip_fresh_fresh by blast
+  from 1 2 show ?thesis by auto
+qed
+
+lemma match_ctor_eqvt_tyvar:
+  fixes a c::"tyvar"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "set (map atom tys) \<sharp>* c" "set (map atom vals) \<sharp>* c"
+  shows "(a \<leftrightarrow> c) \<bullet> MatchCtor D tys vals e = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)"
+proof -
+  from assms(1,3) have 1: "(a \<leftrightarrow> c) \<bullet> tys = tys" using fresh_star_invert flip_fresh_fresh by blast
+  from assms(2,4) have 2: "(a \<leftrightarrow> c) \<bullet> vals = vals" using fresh_star_invert flip_fresh_fresh by blast
+  from 1 2 show ?thesis by auto
+qed
+lemmas match_ctor_eqvt = match_ctor_eqvt_var match_ctor_eqvt_tyvar
+
 (* \<lbrakk> atom x \<sharp> t' ; x = y \<or> atom x \<sharp> t \<rbrakk> \<Longrightarrow> atom x \<sharp> t[t'/y] *)
-lemma fresh_subst_term: "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> e \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_term e e' y"
-  by (nominal_induct e avoiding: x y e' rule: term.strong_induct) auto
-lemma fresh_subst_term_tyvar: "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term e e' y"
-  by (nominal_induct e avoiding: y a e' rule: term.strong_induct) auto
+lemma fresh_subst_term:
+  shows "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> e \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_term e e' y"
+  and "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> alts \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_alt_list alts e' y"
+  and "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> alt \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_alt alt e' y"
+proof (nominal_induct e and alts and alt avoiding: x y e' rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom x \<sharp> e[e'/y]" using fresh_in_match(1) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed auto
+lemma fresh_subst_term_tyvar:
+  shows "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term e e' y"
+  and "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> alts \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_list alts e' y"
+  and "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> alt \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt alt e' y"
+proof (nominal_induct e and alts and alt avoiding: a y e' rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom a \<sharp> e[e'/y]" using fresh_in_match(2) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed auto
 lemma fresh_subst_type: "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> \<sigma> \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_type \<sigma> \<tau> b"
   by (nominal_induct \<sigma> avoiding: a b \<tau> rule: \<tau>.strong_induct) auto
-lemma fresh_subst_term_type: "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term_type e \<tau> b"
-  by (nominal_induct e avoiding: a b \<tau> rule: term.strong_induct) (auto simp: fresh_subst_type)
+lemma fresh_subst_term_type:
+  shows "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term_type e \<tau> b"
+  and "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> alts \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_list_type alts \<tau> b"
+  and "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> alt \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_type alt \<tau> b"
+proof (nominal_induct e and alts and alt avoiding: a b \<tau> rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom a \<sharp> e[\<tau>/b]" using fresh_in_match(2) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed (auto simp: fresh_subst_type)
 lemma fresh_subst_context_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> atom (x::var) \<sharp> subst_context \<Gamma> \<tau>' a"
   by (induction \<Gamma> \<tau>' a rule: subst_context.induct) (auto simp: fresh_Cons)
 lemma fresh_subst_context_tyvar: "\<lbrakk> atom a \<sharp> \<tau>' ; a = b \<or> atom a \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_context \<Gamma> \<tau>' b"
   by (induction \<Gamma> \<tau>' a rule: subst_context.induct) (auto simp: fresh_Cons fresh_Nil fresh_subst_type)
-lemmas fresh_subst = fresh_subst_term fresh_subst_term_tyvar fresh_subst_type fresh_subst_term_type fresh_subst_context_var fresh_subst_context_tyvar
+lemmas fresh_subst = fresh_subst_term(1) fresh_subst_term_tyvar(1) fresh_subst_type fresh_subst_term_type(1) fresh_subst_context_var fresh_subst_context_tyvar fresh_subst_term(2,3) fresh_subst_term_tyvar(2,3) fresh_subst_term_type(2,3)
 
 (* atom c \<sharp> t \<Longrightarrow> t[t'/x] = ((x \<leftrightarrow> c) \<bullet> t)[t'/c] *)
-lemma subst_term_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term e e' x = subst_term ((x \<leftrightarrow> c) \<bullet> e) e' c"
-proof (nominal_induct e avoiding: c x e' rule: term.strong_induct)
+lemma subst_term_var_name:
+  shows "atom c \<sharp> e \<Longrightarrow> subst_term e e' x = subst_term ((x \<leftrightarrow> c) \<bullet> e) e' c"
+  and "atom c \<sharp> alts \<Longrightarrow> subst_alt_list alts e' x = subst_alt_list ((x \<leftrightarrow> c) \<bullet> alts) e' c"
+  and "atom c \<sharp> alt \<Longrightarrow> subst_alt alt e' x = subst_alt ((x \<leftrightarrow> c) \<bullet> alt) e' c"
+proof (nominal_induct e and alts and alt avoiding: c x e' rule: term_alt_list_alt.strong_induct)
   case (Let y \<tau> e1 e2)
   then have "(Let y \<tau> e1 e2)[e'/x] = Let y \<tau> e1[e'/x] e2[e'/x]" by auto
   also have "... = Let y \<tau> ((x \<leftrightarrow> c) \<bullet> e1)[e'/c] ((x \<leftrightarrow> c) \<bullet> e2)[e'/c]"
-    by (metis Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(7))
+    by (metis Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(7))
   also have "... = (Let y \<tau> ((x \<leftrightarrow> c) \<bullet> e1) ((x \<leftrightarrow> c) \<bullet> e2))[e'/c]" by (simp add: Let.hyps(1) Let.hyps(3))
   finally show ?case
-    by (metis Let.hyps(1) Let.hyps(2) flip_fresh_fresh fresh_at_base(2) no_vars_in_ty term.perm_simps(7))
+    by (metis Let.hyps(1) Let.hyps(2) flip_fresh_fresh fresh_at_base(2) no_vars_in_ty term_alt_list_alt.perm_simps(7))
+next
+  case (MatchCtor D tys vals e)
+  from MatchCtor have "(MatchCtor D tys vals e)[e'/x] = MatchCtor D tys vals e[e'/x]" using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by auto
+  also have "... = MatchCtor D tys vals ((x \<leftrightarrow> c) \<bullet> e)[e'/c]" using fresh_in_match(1) MatchCtor by metis
+  also have "... = (MatchCtor D tys vals ((x \<leftrightarrow> c) \<bullet> e))[e'/c]" using fresh_match_Pair[OF MatchCtor(3,6,1,4)] by simp
+  finally show ?case using match_ctor_eqvt(1)[OF MatchCtor(2,5,1,4)] by presburger
 qed (auto simp: flip_fresh_fresh fresh_at_base)
 
 lemma subst_type_var_name: "atom c \<sharp> \<sigma> \<Longrightarrow> subst_type \<sigma> \<tau> a = subst_type ((a \<leftrightarrow> c) \<bullet> \<sigma>) \<tau> c"
@@ -38,12 +111,15 @@ proof (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct)
   finally show ?case by (metis TyForall.hyps(1) TyForall.hyps(2) \<tau>.perm_simps(5) flip_fresh_fresh fresh_at_base(2) no_tyvars_in_kinds)
 qed (auto simp: fresh_at_base)
 
-lemma subst_term_type_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type ((a \<leftrightarrow> c) \<bullet> e) \<tau> c"
-proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
+lemma subst_term_type_var_name:
+  shows "atom c \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type ((a \<leftrightarrow> c) \<bullet> e) \<tau> c"
+  and "atom c \<sharp> alts \<Longrightarrow> subst_alt_list_type alts \<tau> a = subst_alt_list_type ((a \<leftrightarrow> c) \<bullet> alts) \<tau> c"
+  and "atom c \<sharp> alt \<Longrightarrow> subst_alt_type alt \<tau> a = subst_alt_type ((a \<leftrightarrow> c) \<bullet> alt) \<tau> c"
+proof (nominal_induct e and alts and alt avoiding: c a \<tau> rule: term_alt_list_alt.strong_induct)
   case (Lam x \<tau>1 e)
   then have "(\<lambda> x:\<tau>1. e)[\<tau>/a] = (\<lambda> x:\<tau>1[\<tau>/a]. e[\<tau>/a])" by simp
   also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. e[\<tau>/a])" using subst_type_var_name Lam by force
-  also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c])" using Lam by (metis fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(5))
+  also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c])" using Lam by (metis fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(5))
   also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1). ((a \<leftrightarrow> c) \<bullet> e))[\<tau>/c]" by simp
   finally show ?case by (simp add: Lam.hyps(2) flip_fresh_fresh)
 next
@@ -51,11 +127,16 @@ next
   then have "(Let x \<tau>1 e1 e2)[\<tau>/a] = Let x \<tau>1[\<tau>/a] e1[\<tau>/a] e2[\<tau>/a]" by simp
   also have "... = Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c] e1[\<tau>/a] e2[\<tau>/a]" using subst_type_var_name Let by auto
   also have "... = Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c] ((a \<leftrightarrow> c) \<bullet> e1)[\<tau>/c] ((a \<leftrightarrow> c) \<bullet> e2)[\<tau>/c]"
-    by (metis (mono_tags, lifting) Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(7))
+    by (metis (mono_tags, lifting) Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(7))
   also have "... = (Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1) ((a \<leftrightarrow> c) \<bullet> e1) ((a \<leftrightarrow> c) \<bullet> e2))[\<tau>/c]" by simp
   finally show ?case by (simp add: flip_fresh_fresh)
+next
+  case (MatchCtor D tys vals e)
+  have "(MatchCtor D tys vals e)[\<tau>/a] = MatchCtor D tys vals e[\<tau>/a]" using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+  also have "... = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c]" using fresh_in_match(2) MatchCtor by metis
+  also have "... = (MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e))[\<tau>/c]" using fresh_match_Pair[OF MatchCtor(3,6,1,4)] by simp
+  finally show ?case using match_ctor_eqvt(2)[OF MatchCtor(2,5,1,4)] by presburger
 qed (auto simp: flip_fresh_fresh fresh_at_base subst_type_var_name)
-lemmas subst_var_name = subst_term_var_name subst_type_var_name subst_term_type_var_name
 
 lemma subst_context_var_name: "atom c \<sharp> \<Gamma> \<Longrightarrow> subst_context \<Gamma> \<tau> a = subst_context ((a \<leftrightarrow> c) \<bullet> \<Gamma>) \<tau> c"
 proof (induction \<Gamma> \<tau> a rule: subst_context.induct)
@@ -74,14 +155,15 @@ proof (induction \<Gamma> \<tau> a rule: subst_context.induct)
     show ?thesis using a b c 1 by argo
   qed
 qed (auto simp: flip_fresh_fresh fresh_Cons subst_type_var_name)
+lemmas subst_var_name = subst_term_var_name(1) subst_type_var_name subst_term_type_var_name(1) subst_context_var_name subst_term_var_name(2,3) subst_term_type_var_name(2,3)
 
 (* [[atom a]]lst. t = [[atom a2]]lst. t2 \<Longrightarrow> subst t t' a = subst t2 t' a2 *)
 lemma subst_term_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term e t a = subst_term e' t a'"
-  by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name)
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name(1))
 lemma subst_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_type e \<tau> a = subst_type e' \<tau> a'"
   by (metis Abs1_eq_iff(3) flip_commute subst_type_var_name)
 lemma subst_term_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type e' \<tau> a'"
-  by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name(1))
 lemmas subst_same = subst_term_same subst_type_same subst_term_type_same
 
 (* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
@@ -91,15 +173,23 @@ lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>is
 lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BVar x \<tau>) \<Gamma>"
   apply (induction \<Gamma>) apply simp
   by (metis (mono_tags, lifting) binder.fresh(1) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(2) isin.simps(3))
+lemmas fresh_not_isin = fresh_not_isin_tyvar fresh_not_isin_var
 
 (* atom x \<sharp> t \<Longrightarrow> subst t' x t = t *)
-lemma fresh_subst_term_same: "atom x \<sharp> e \<Longrightarrow> subst_term e e' x = e"
-proof (induction e e' x rule: subst_term.induct)
-  case (5 y e x \<tau> e2)
+lemma fresh_subst_term_same:
+  shows "atom x \<sharp> e \<Longrightarrow> subst_term e e' x = e"
+  and "atom x \<sharp> alts \<Longrightarrow> subst_alt_list alts e' x = alts"
+  and "atom x \<sharp> alt \<Longrightarrow> subst_alt alt e' x = alt"
+proof (induction e e' x and alts e' x and alt e' x rule: subst_term_subst_alt_list_subst_alt.induct)
+  case (6 y e x \<tau> e2)
   then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
 next
-  case (7 y e x \<tau> e1 e2)
+  case (8 y e x \<tau> e1 e2)
   then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
+next
+  case (11 tys vals e x D t)
+  then have "atom x \<sharp> t" by (meson fresh_PairD(2) fresh_at_base(2) fresh_star_def term_alt_list_alt.fresh(11))
+  then show ?case using 11 by simp
 qed auto
 
 lemma fresh_subst_type_same: "atom a \<sharp> \<sigma> \<Longrightarrow> subst_type \<sigma> \<tau> a = \<sigma>"
@@ -109,33 +199,137 @@ proof (induction \<sigma> \<tau> a rule: subst_type.induct)
     using fresh_Pair fresh_at_base(2) fresh_def list.set(1) list.set(2) subst_type.simps(4) by fastforce
 qed auto
 
-lemma fresh_subst_term_type_same: "atom a \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = e"
-proof (induction e \<tau> a rule: subst_term_type.induct)
-  case (6 b \<tau> a k e2)
-  then show ?case by (simp add: "6.hyps" fresh_Pair fresh_at_base(2))
+lemma fresh_subst_term_type_same:
+  shows "atom a \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = e"
+  and "atom a \<sharp> alts \<Longrightarrow> subst_alt_list_type alts \<tau> a = alts"
+  and "atom a \<sharp> alt \<Longrightarrow> subst_alt_type alt \<tau> a = alt"
+proof (induction e \<tau> a and alts \<tau> a and alt \<tau> a rule: subst_term_type_subst_alt_list_type_subst_alt_type.induct)
+  case (7 b \<tau> a k e2)
+  then show ?case by (simp add: "7.hyps" fresh_Pair fresh_at_base(2))
+next
+  case (11 tys vals \<tau> a D e)
+  then have "atom a \<sharp> e" by (meson fresh_PairD(2) fresh_at_base(2) fresh_star_def term_alt_list_alt.fresh(11))
+  then show ?case using 11 by auto
 qed (auto simp: fresh_subst_type_same)
 
 lemma fresh_subst_context_same: "atom a \<sharp> \<Gamma> \<Longrightarrow> subst_context \<Gamma> \<tau> a = \<Gamma>"
   by (induction \<Gamma> \<tau> a rule: subst_context.induct) (auto simp: fresh_Cons fresh_subst_type_same)
 
-lemmas fresh_subst_same = fresh_subst_term_same fresh_subst_type_same fresh_subst_term_type_same fresh_subst_context_same
+lemmas fresh_subst_same = fresh_subst_term_same(1) fresh_subst_type_same fresh_subst_term_type_same(1) fresh_subst_context_same fresh_subst_term_same(2,3) fresh_subst_term_type_same(2,3)
 
 (* \<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst (subst e t2 x) t1 y = subst (subst e t1 y) (subst t2 t1 y) x *)
-lemma subst_subst_term: "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_term (subst_term e t2 x) t1 y = subst_term (subst_term e t1 y) (subst_term t2 t1 y) x"
-  by (nominal_induct e avoiding: x y t1 t2 rule: term.strong_induct) (auto simp: fresh_subst_same fresh_subst)
+lemma subst_subst_term:
+  shows "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_term (subst_term e t2 x) t1 y = subst_term (subst_term e t1 y) (subst_term t2 t1 y) x"
+  and "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_alt_list (subst_alt_list alts t2 x) t1 y = subst_alt_list (subst_alt_list alts t1 y) (subst_term t2 t1 y) x"
+  and "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_alt (subst_alt alt t2 x) t1 y = subst_alt (subst_alt alt t1 y) (subst_term t2 t1 y) x"
+proof (nominal_induct e and alts and alt avoiding: x y t1 t2 rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  have 1: "set (map atom tys) \<sharp>* t2[t1/y]" unfolding fresh_star_def using fresh_subst(2) by (metis MatchCtor(3,4) ex_map_conv fresh_star_def)
+  have 2: "set (map atom vals) \<sharp>* t2[t1/y]" unfolding fresh_star_def using fresh_subst(1) by (metis MatchCtor(7,8) ex_map_conv fresh_star_def)
+  have "(MatchCtor D tys vals e)[t2/x][t1/y] = MatchCtor D tys vals e[t2/x][t1/y]" using fresh_match_Pair[OF MatchCtor(4,8,1,5)] fresh_match_Pair[OF MatchCtor(3,7,2,6)] by simp
+  also have "... = MatchCtor D tys vals e[t1/y][t2[t1/y]/x]" using MatchCtor by simp
+  finally show ?case using fresh_match_Pair[OF MatchCtor(3,7,2,6)] fresh_match_Pair[OF 1 2 MatchCtor(1,5)] by simp
+qed (auto simp: fresh_subst_same fresh_subst)
 lemma subst_subst_type: "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_type (subst_type \<sigma> \<tau>2 a) \<tau>1 b = subst_type (subst_type \<sigma> \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
   by (nominal_induct \<sigma> avoiding: a b \<tau>1 \<tau>2 rule: \<tau>.strong_induct) (auto simp: fresh_subst_same fresh_subst)
-lemma subst_subst_term_type: "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_term_type (subst_term_type e \<tau>2 a) \<tau>1 b = subst_term_type (subst_term_type e \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
-  by (nominal_induct e avoiding: a b \<tau>1 \<tau>2 rule: term.strong_induct) (auto simp: fresh_subst_same fresh_subst subst_subst_type)
+lemma subst_subst_term_type:
+  shows "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_term_type (subst_term_type e \<tau>2 a) \<tau>1 b = subst_term_type (subst_term_type e \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+  and "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_alt_list_type (subst_alt_list_type alts \<tau>2 a) \<tau>1 b = subst_alt_list_type (subst_alt_list_type alts \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+  and "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_alt_type (subst_alt_type alt \<tau>2 a) \<tau>1 b = subst_alt_type (subst_alt_type alt \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+proof (nominal_induct e and alts and alt avoiding: a b \<tau>1 \<tau>2 rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  have 1: "set (map atom tys) \<sharp>* \<tau>2[\<tau>1/b]" unfolding fresh_star_def using fresh_subst(3) by (metis MatchCtor(3,4) ex_map_conv fresh_star_def)
+  have 2: "set (map atom vals) \<sharp>* \<tau>2[\<tau>1/b]" unfolding fresh_star_def by simp
+  have "(MatchCtor D tys vals e)[\<tau>2/a][\<tau>1/b] = MatchCtor D tys vals e[\<tau>2/a][\<tau>1/b]" using fresh_match_Pair[OF MatchCtor(4,8,1,5)] fresh_match_Pair[OF MatchCtor(3,7,2,6)] by simp
+  also have "... = MatchCtor D tys vals e[\<tau>1/b][\<tau>2[\<tau>1/b]/a]" using MatchCtor by simp
+  finally show ?case using fresh_match_Pair[OF MatchCtor(3,7,2,6)] fresh_match_Pair[OF 1 2 MatchCtor(1,5)] by simp
+qed (auto simp: fresh_subst_same fresh_subst subst_subst_type)
 lemma subst_subst_context: "\<lbrakk> a \<noteq> b; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_context (subst_context \<Gamma> \<tau>2 a) \<tau>1 b = subst_context (subst_context \<Gamma> \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
   by (induction \<Gamma> \<tau>2 a rule: subst_context.induct) (auto simp: subst_subst_type)
-lemmas subst_subst = subst_subst_term subst_subst_type subst_subst_term_type subst_subst_context
+lemmas subst_subst = subst_subst_term(1) subst_subst_type subst_subst_term_type(1) subst_subst_context subst_subst_term(2,3) subst_subst_term_type(2,3)
 
 (* misc *)
 lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
   by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
 
 lemma head_ctor_is_value: "head_ctor e \<Longrightarrow> is_value e"
-  by (induction e rule: term.induct) auto
+  by (induction e rule: term_alt_list_alt.inducts(1)) auto
+
+lemma strengthen_isin_tyvar: "isin (BTyVar a k) (\<Gamma>' @ BVar x \<tau> # \<Gamma>) \<Longrightarrow> isin (BTyVar a k) (\<Gamma>' @ \<Gamma>)"
+proof (induction \<Gamma>')
+  case (Cons a \<Gamma>')
+  then show ?case by (cases a rule: binder.exhaust) auto
+qed auto
+
+lemma isin_split: "isin bndr \<Gamma> \<Longrightarrow> \<exists>\<Gamma>1 \<Gamma>2. \<Gamma> = \<Gamma>1 @ bndr # \<Gamma>2"
+proof (induction \<Gamma>)
+  case (Cons a \<Gamma>)
+  then show ?case
+  proof (cases "a = bndr")
+    case True
+    then show ?thesis by blast
+  next
+    case False
+    then have "isin bndr \<Gamma>" using Cons(2)
+      by (cases a rule: binder.exhaust; cases bndr rule: binder.exhaust) auto
+    then show ?thesis using Cons(1) by (metis Cons_eq_appendI)
+  qed
+qed simp
+
+lemma supp_subst_type: "supp (subst_type \<tau> \<sigma> a) \<subseteq> (supp \<tau> - {atom a}) \<union> supp \<sigma>"
+proof (induction \<tau> \<sigma> a rule: subst_type.induct)
+  case (2 b \<tau> a)
+  then show ?case by (cases "b = a") (auto simp: supp_at_base \<tau>.supp(1))
+qed (auto simp: \<tau>.supp pure_supp)
+
+lemma supp_head_data: "head_data \<tau> = Some (T, \<sigma>s) \<Longrightarrow> supp \<sigma>s \<subseteq> supp \<tau>"
+proof (induction \<tau> arbitrary: \<sigma>s rule: head_data.induct)
+  case (2 T)
+  then show ?case using \<tau>.supp(2) pure_supp supp_Nil by auto
+next
+  case (4 \<tau>1 \<tau>2)
+  then obtain xs where P: "head_data \<tau>1 = Some (T, xs)" by (auto split!: option.splits)
+  then have 1: "supp xs \<subseteq> supp \<tau>1" by (rule 4(1))
+  from 4(2) P have "\<sigma>s = xs @ [\<tau>2]" by auto
+  then show ?case using 1 supp_append supp_Nil supp_Cons unfolding \<tau>.supp(4) by blast
+qed auto
+
+lemma supp_zip_with_var: "supp (zip_with BVar vals args) \<subseteq> supp vals \<union> supp args"
+proof (induction vals arbitrary: args)
+  case Nil
+  then show ?case using supp_Nil by auto
+next
+  case (Cons a vals)
+  then show ?case by (cases args) (auto simp: supp_Nil supp_Cons binder.supp)
+qed
+
+lemma supp_zip_with_tyvar: "supp (zip_with BTyVar tys ks) \<subseteq> supp tys \<union> supp ks"
+proof (induction tys arbitrary: ks)
+  case Nil
+  then show ?case using supp_Nil by auto
+next
+  case (Cons a vals)
+  then show ?case by (cases ks) (auto simp: supp_Nil supp_Cons binder.supp)
+qed
+lemmas supp_zip_with = supp_zip_with_var supp_zip_with_tyvar
+
+lemma supp_vars: "supp (vars::var list) = set (map atom vars)"
+  by (induction vars) (auto simp: supp_Nil supp_Cons supp_at_base)
+lemma supp_tyvars: "supp (tyvars::tyvar list) = set (map atom tyvars)"
+  by (induction tyvars) (auto simp: supp_Nil supp_Cons supp_at_base)
+
+lemma permute_atoms_split:
+  fixes tys tys2::"tyvar list" and vars vars2::"var list"
+  assumes "p \<bullet> (map atom tys2 @ map atom vars2) = map atom tys @ map atom vars"
+  shows "p \<bullet> tys2 = tys" "p \<bullet> vars2 = vars"
+proof -
+  have 1: "map atom (p \<bullet> tys2) @ map atom (p \<bullet> vars2) = map atom tys @ map atom vars" (is "?L = ?R")
+    using assms by simp
+  then have "get_tyvars ?L = get_tyvars ?R" by simp
+  then show "p \<bullet> tys2 = tys" using get_tyvars_append by auto
+
+  from 1 have "get_vars ?L = get_vars ?R" by simp
+  then show "p \<bullet> vars2 = vars" using get_vars_append by auto
+qed
 
 end
diff --git a/Nominal2_Lemmas.thy b/Nominal2_Lemmas.thy
index 421adae..57cb3d2 100644
--- a/Nominal2_Lemmas.thy
+++ b/Nominal2_Lemmas.thy
@@ -62,6 +62,19 @@ proof -
   show ?thesis using 1 2 3 equal by argo
 qed
 
+lemma Abs_sumC_star:
+  fixes ys ys'::"atom list" and x x'::"'a::fs" and e e'::"'b::fs" and e2 e2'::"'c::fs" and f::"'c * 'b * 'a \<Rightarrow> 'd::fs"
+  assumes fresh: "set ys \<sharp>* (e, x)" "set ys' \<sharp>* (e', x')"
+  and eqvt_at: "eqvt_at f (e2, e, x)" "eqvt_at f (e2', e', x')"
+  and equal: "[ys]lst. e2 = [ys']lst. e2'" "x = x'" "e = e'"
+  shows "[ys]lst. f (e2, e, x) = [ys']lst. f (e2', e', x')"
+proof -
+  have 1: "set ys \<sharp>* ([ys]lst. f (e2, e, x))" by (simp add: Abs_fresh_star(3))
+  have 2: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys]lst. f (e2, e, x)) = [p \<bullet> ys]lst. f (p \<bullet> e2, e, x)" using eqvt_at(1) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
+  have 3: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys']lst. f (e2', e, x)) = [p \<bullet> ys']lst. f (p \<bullet> e2', e, x)" using eqvt_at(2) equal(2,3) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
+  show ?thesis using Abs_lst_fcb2[where f="\<lambda>a b c. [a]lst. f (b, e, x)", OF equal(1) 1 fresh(1) _ 2 3] fresh(2) equal(2,3) by simp
+qed
+
 lemma Abs_fresh_var:
   fixes y::"'a::at" and e ::"'b::fs"
   obtains c::"'a" and e'::"'b" where "([[atom y]]lst. e = [[atom c]]lst. e') \<and> atom y \<sharp> [[atom c]]lst. e'"
@@ -79,7 +92,30 @@ lemma Abs_rename_body:
   shows "(a \<leftrightarrow> b) \<bullet> e1 = e2"
   by (metis Abs1_eq_iff'(3) Nominal2_Base.swap_self assms flip_commute flip_def fresh_star_zero supp_perm_eq_test)
 
+lemma Abs_rename_body_star:
+  fixes as bs::"atom list" and e1 e2::"'b::fs"
+  assumes "[as]lst. e1 = [bs]lst. e2"
+  obtains p where "p \<bullet> e1 = e2" "p \<bullet> as = bs" "supp p \<subseteq> set as \<union> set bs"
+  by (metis (full_types) Abs_eq_iff2(3) alpha_lst.simps assms)
+
 lemma fresh_filter: "a = b \<or> atom a \<sharp> xs \<Longrightarrow> atom a \<sharp> filter (\<lambda>x. x \<noteq> b) xs"
   by (induction xs) (auto simp: fresh_Cons fresh_Nil)
 
+lemma Projl_permute: "\<exists>y. f = Inl y \<Longrightarrow> p \<bullet> projl f = projl (p \<bullet> f)" by auto
+lemma Projr_permute: "\<exists>y. f = Inr y \<Longrightarrow> p \<bullet> projr f = projr (p \<bullet> f)" by auto
+
+lemma pair3_eqvt[simp]: "(a \<leftrightarrow> b) \<bullet> (x, y, z) = ((a \<leftrightarrow> b) \<bullet> x, (a \<leftrightarrow> b) \<bullet> y, (a \<leftrightarrow> b) \<bullet> z)"
+  by (simp split: prod.splits)
+
+lemma eqvt_fBall[eqvt]: "p \<bullet> fBall s f = fBall (p \<bullet> s) (p \<bullet> f)"
+  apply auto
+  apply (metis eqvt_bound eqvt_lambda fBallE in_fset_eqvt permute_pure)
+  by (metis eqvt_apply fBallE fBallI in_fset_eqvt permute_pure)
+
+lemma permute_length:
+  fixes xs ys::"'a::at list"
+  assumes "p \<bullet> xs = ys"
+  shows "length xs = length ys"
+using assms by (induction xs arbitrary: ys) auto
+
 end
diff --git a/Semantics.thy b/Semantics.thy
index 234a189..ba0f749 100644
--- a/Semantics.thy
+++ b/Semantics.thy
@@ -18,6 +18,8 @@ inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightar
 
 | ST_Let: "Let x \<tau> e1 e2 \<longrightarrow> e2[e1/x]"
 
+| ST_Case_Cong: "e \<longrightarrow> e' \<Longrightarrow> Case e alts \<longrightarrow> Case e' alts"
+
 equivariance Step
 nominal_inductive Step .
 
@@ -45,7 +47,7 @@ next
   show ?case
   proof (rule ccontr)
     assume "\<not>beta_nf (TApp e \<tau>)"
-    then obtain e' where "TApp e \<tau> \<longrightarrow> e'" using beta_nf_def by blast
+    then obtain e' where "TApp e \<tau> \<longrightarrow> e'" using beta_nf_def (* by blast*)
     then show "False" using TApp head_ctor_is_value beta_nf_def by cases auto
   qed
 next
diff --git a/Syntax.thy b/Syntax.thy
index 837495b..d0525f4 100644
--- a/Syntax.thy
+++ b/Syntax.thy
@@ -23,6 +23,12 @@ nominal_datatype "\<kappa>" =
   Star ("\<star>")
   | KArrow "\<kappa>" "\<kappa>" (infixr "\<rightarrow>" 50)
 
+instance \<kappa> :: pure
+proof (standard, goal_cases)
+  case (1 p x)
+  then show ?case by (induction x rule: \<kappa>.induct) auto
+qed
+
 nominal_datatype "\<tau>" =
   TyVar "tyvar"
   | TyData "data_name"
@@ -41,6 +47,15 @@ nominal_datatype "term" =
  | Lam x::"var" "\<tau>" e::"term" binds x in e  ("\<lambda> _ : _ . _" 50)
  | TyLam a::"tyvar" "\<kappa>" e::"term" binds a in e ("\<Lambda> _ : _ . _" 50)
  | Let x::"var" "\<tau>" "term" e2::"term" binds x in e2
+ | Case "term" "alt_list"
+and "alt_list" =
+  ANil
+| ACons "alt" "alt_list"
+and "alt" =
+  MatchCtor "ctor_name" tys::"tyvar list" vals::"var list" e::"term" binds tys vals in e
+lemmas term_supp = term_alt_list_alt.supp(1-8)
+lemmas alt_list_supp = term_alt_list_alt.supp(9,10)
+lemmas alt_supp = term_alt_list_alt.supp(11)
 
 nominal_datatype "binder" =
   BVar "var" "\<tau>"
@@ -75,6 +90,8 @@ lemma no_tyvars_in_kinds[simp]: "atom (a :: tyvar) \<sharp> (k :: \<kappa>)"
 
 lemma supp_empty_kinds[simp]: "supp (k :: \<kappa>) = {}"
   by (induction k rule: \<kappa>.induct) (auto simp: \<kappa>.supp)
+lemma supp_empty_kind_list[simp]: "supp (ks :: \<kappa> list) = {}"
+  by (induction ks) (auto simp: supp_Nil supp_Cons)
 
 lemma perm_data_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (T :: data_name) = T"
   using flip_fresh_fresh pure_fresh by blast
@@ -84,6 +101,13 @@ lemma perm_ctor_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (D ::
   using flip_fresh_fresh pure_fresh by blast
 lemma perm_ctor_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
   using flip_fresh_fresh pure_fresh by blast
-
+lemma perm_kind_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (k::\<kappa>) = k"
+  using supp_empty_kinds flip_fresh_fresh fresh_def by blast
+lemma perm_kind_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (k::\<kappa>) = k"
+  using supp_empty_kinds flip_fresh_fresh fresh_def by blast
+lemma perm_kind_list_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (ks::\<kappa> list) = ks"
+  by (induction ks) auto
+lemma perm_kind_list_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (ks::\<kappa> list) = ks"
+  by (induction ks) auto
 
 end
diff --git a/Typing.thy b/Typing.thy
index cfddac9..08b7c4a 100644
--- a/Typing.thy
+++ b/Typing.thy
@@ -1,5 +1,5 @@
 theory Typing
-  imports Syntax Defs Lemmas
+  imports Syntax Defs Defs2 Lemmas
 begin
 
 no_notation Set.member  ("(_/ : _)" [51, 51] 50)
@@ -12,7 +12,7 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
 
 | Ax_Data: "\<lbrakk> \<turnstile> \<Delta> ; \<nexists>k. AxData T k \<in> set \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxData T \<kappa> # \<Delta>"
 
-| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some T ; \<nexists>t. AxCtor D t \<in> set \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
+| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some (T, ks) ; \<nexists>t. AxCtor D t \<in> set \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
 
 (* ------------------------------ *)
 
@@ -36,6 +36,11 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
 
 equivariance Ax
 
+syntax
+  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+translations
+  "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST fBall A (\<lambda>x. P)"
+
 inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow> \<tau> \<Rightarrow> bool" ("_ , _ \<turnstile> _ : _" 50) where
   Tm_Var: "\<lbrakk> \<Delta> \<turnstile> \<Gamma> ; BVar x \<tau> \<in> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> (Var x) : \<tau>"
 
@@ -51,6 +56,15 @@ inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow
 
 | Tm_Let: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e1 : \<tau>1 ; BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e2 : \<tau>2 \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Let x \<tau>1 e1 e2 : \<tau>2"
 
+| Tm_Case: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; head_data \<tau>1 = Some (T, \<sigma>s) ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; exhaustive alts \<Delta> T ;
+            \<forall>alt |\<in>| set_alts alts. (\<exists>K tys vals e' cty ks args \<Gamma>'.
+                alt = MatchCtor K tys vals e' \<and>
+                AxCtor K cty \<in> set \<Delta> \<and> ctor_type cty = Some (T, ks) \<and>
+                subst_ctor cty \<sigma>s = Some args \<and>
+                \<Gamma>' = zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma> \<and>
+                \<Gamma>' , \<Delta> \<turnstile> e' : \<tau>
+              ) \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Case e alts : \<tau>"
+
 equivariance Tm
 
 lemmas Ax_intros = Ax_Ctx_Ty.intros(1-3)
@@ -76,6 +90,7 @@ inductive_cases TmE[elim!]:
   "\<Gamma> , \<Delta> \<turnstile> App e1 e2 : \<tau>2"
   "\<Gamma> , \<Delta> \<turnstile> TApp e \<tau> : \<tau>2"
   "\<Gamma> , \<Delta> \<turnstile> Ctor D : \<tau>"
+  "\<Gamma> , \<Delta> \<turnstile> Case e alts : \<tau>"
 
 (* Split induction principles *)
 lemma Ty_induct[consumes 1, case_names Var App Data Arrow Forall]:
@@ -168,6 +183,33 @@ proof -
   then show "\<Delta> \<turnstile> \<Gamma>' @ \<Gamma> \<longrightarrow> P \<Delta> \<Gamma>'" and "\<Gamma>' @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<longrightarrow> Q \<Gamma>' \<Delta> \<tau> k2" by simp_all
 qed
 
+lemma alts_induct[consumes 1, case_names MatchCtor]:
+  assumes "\<forall>alt |\<in>| set_alts alts. (\<exists>K tys vals e' cty ks args \<Gamma>'.
+                alt = MatchCtor K tys vals e' \<and>
+                AxCtor K cty \<in> set \<Delta> \<and> ctor_type cty = Some (T, ks) \<and>
+                subst_ctor cty \<sigma>s = Some args \<and>
+                \<Gamma>' = zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma> \<and>
+                \<Gamma>' , \<Delta> \<turnstile> e' : \<tau> \<and> P \<Gamma>' e'
+              )"
+  and "\<And>K tys vals e' cty ks args. \<lbrakk> AxCtor K cty \<in> set \<Delta> ; ctor_type cty = Some (T, ks) ; subst_ctor cty \<sigma>s = Some args ;
+        zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma> , \<Delta> \<turnstile> e' : \<tau> ; P (zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma>) e' \<rbrakk> \<Longrightarrow> Q \<Gamma> (MatchCtor K tys vals e')"
+shows "\<forall>alt |\<in>| set_alts alts. Q \<Gamma> alt"
+proof -
+  let ?W = "\<lambda>alt. (\<exists>K tys vals e' cty ks args \<Gamma>'.
+                alt = MatchCtor K tys vals e' \<and>
+                AxCtor K cty \<in> set \<Delta> \<and> ctor_type cty = Some (T, ks) \<and>
+                subst_ctor cty \<sigma>s = Some args \<and>
+                \<Gamma>' = zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma> \<and>
+                \<Gamma>' , \<Delta> \<turnstile> e' : \<tau> \<and> P \<Gamma>' e')"
+  show ?thesis
+  using assms(1) proof (induction alts rule: term_alt_list_alt.inducts(2)[of "\<lambda>_. True" _ "\<lambda>alt. ?W alt \<longrightarrow> Q \<Gamma> alt"])
+  next
+    case (MatchCtor K tys vals e')
+    then show ?case using assms(2) apply auto
+      by (metis term_alt_list_alt.eq_iff(11))
+  qed simp_all
+qed
+
 (* context validity *)
 lemma context_valid_ty: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<kappa> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>"
   by (induction \<Gamma> \<Delta> \<tau> \<kappa> rule: Ty_induct) auto
@@ -175,49 +217,41 @@ lemma context_valid_tm: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longright
   by (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct) (auto simp: context_valid_ty)
 lemmas context_valid = context_valid_ty context_valid_tm
 
-(* \<lbrakk> \<Gamma> \<turnstile> e : t ; atom x \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom x \<sharp> e *)
-lemma fresh_in_context_ty: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> \<tau>"
+lemma supp_in_context_ty: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k \<Longrightarrow> supp \<tau> \<subseteq> supp \<Gamma>"
 proof (induction \<Gamma> \<Delta> \<tau> k rule: Ty_induct)
   case (Var \<Gamma> \<Delta> a k)
-  then show ?case using fresh_at_base(2) fresh_not_isin_tyvar by fastforce
-qed (auto simp: fresh_Cons)
-
-lemma fresh_in_context_term_var: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (x::var) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom x \<sharp> e"
-proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct)
-case (Tm_Var \<Gamma> \<Delta> x \<tau>)
-  then show ?case using fresh_ineq_at_base fresh_not_isin_var by force
-qed (auto simp: fresh_Cons)
-
-lemma fresh_in_context_term_tyvar: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> e"
-proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct)
-  case (Tm_Abs x \<tau>1 \<Gamma> \<Delta> e \<tau>2)
-  then have "atom a \<sharp> \<tau>1" by (meson CtxE(2) context_valid_tm fresh_in_context_ty)
-  then show ?case by (simp add: Tm_Abs fresh_Cons)
+  then show ?case by (metis \<tau>.supp(1) fresh_def fresh_not_isin_tyvar singletonD subsetCI supp_at_base)
 next
-  case (Tm_Let \<Gamma> e1 e2 \<tau>1 \<tau>2 x)
-  then show ?case
-    by (metis (mono_tags, lifting) CtxE(2) binder.fresh(1) context_valid_tm fresh_Cons fresh_in_context_ty fresh_ineq_at_base list.set_intros(1) term.fresh(7))
-qed (auto simp: fresh_Cons fresh_in_context_ty)
-lemmas fresh_in_context = fresh_in_context_ty fresh_in_context_term_var fresh_in_context_term_tyvar
+  case (Forall \<Gamma> \<Delta> a k \<sigma>)
+  from Forall(2) show ?case unfolding supp_Cons binder.supp(2) \<tau>.supp(5) pure_supp supp_at_base by auto
+qed (auto simp: \<tau>.supp pure_supp)
 
-lemma fresh_in_axioms: "\<turnstile> \<Delta> \<Longrightarrow> atom (a::tyvar) \<sharp> \<Delta>"
-proof -
-  fix \<Gamma> \<tau> k
-  assume a: "\<turnstile> \<Delta>"
-  let ?Q = "\<lambda>b c d e. atom a \<sharp> c"
-  let ?W = "\<lambda>b c. atom a \<sharp> b"
-
-  have "(\<turnstile> \<Delta> \<longrightarrow> atom a \<sharp> \<Delta>) \<and> (\<Delta> \<turnstile> \<Gamma> \<longrightarrow> ?W \<Delta> \<Gamma>) \<and> (\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k \<longrightarrow> ?Q \<Gamma> \<Delta> \<tau> k)"
-  proof (induction rule: Ax_Ctx_Ty.induct[of "\<lambda>x. atom a \<sharp> x" ?Q ?W])
-    case (Ax_Ctor \<Delta> \<tau> D)
-    then show ?case using fresh_in_context(1)[OF Ax_Ctor(1) fresh_Nil] fresh_Cons fresh_Nil by fastforce
-  qed (auto simp: fresh_Nil fresh_Cons)
-
-  then show ?thesis using a by simp
-qed
+corollary fresh_in_context_ty: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> \<tau>"
+  unfolding fresh_def using supp_in_context_ty by blast
+
+lemma axioms_cons_valid[elim]: "\<turnstile> ax # \<Delta> \<Longrightarrow> (\<turnstile> \<Delta> \<Longrightarrow> P) \<Longrightarrow> P"
+  by (cases rule: Ax.cases) (auto simp: axioms_valid(2))
 
-lemma perm_axioms_tyvars[simp]: "\<turnstile> \<Delta> \<Longrightarrow> ((a::tyvar) \<leftrightarrow> b) \<bullet> \<Delta> = \<Delta>"
-  using flip_fresh_fresh fresh_in_axioms by blast
+lemma axioms_empty_supp: "\<turnstile> \<Delta> \<Longrightarrow> supp \<Delta> = {}"
+proof (induction \<Delta>)
+  case (Cons a \<Delta>)
+  then show ?case
+  proof (cases a rule: axiom.exhaust)
+    case (AxData D k)
+    then show ?thesis by (metis AxE(1) Cons.IH Cons.prems axiom.supp(1) pure_supp supp_Cons)
+  next
+    case (AxCtor K \<tau>)
+    then have "[] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>" using Cons by blast
+    then have 1: "supp \<tau> = {}" using supp_in_context_ty supp_Nil by blast
+    have 2: "supp \<Delta> = {}" using Cons by auto
+    then show ?thesis using 1 AxCtor axiom.supp(2) pure_supp unfolding supp_Cons by blast
+  qed
+qed (simp add: supp_Nil)
+
+corollary fresh_in_axioms: "\<turnstile> \<Delta> \<Longrightarrow> atom (a::tyvar) \<sharp> \<Delta>"
+  unfolding fresh_def using axioms_empty_supp by simp
+corollary permute_axioms[simp]: "\<turnstile> \<Delta> \<Longrightarrow> p \<bullet> \<Delta> = \<Delta>"
+  using axioms_empty_supp by (simp add: fresh_star_def supp_perm_eq)
 
 nominal_inductive Ax avoids
   Ty_Forall: a
@@ -231,7 +265,425 @@ proof goal_cases
   then show ?case using 2 fresh_star_def by fastforce
 qed auto
 
-nominal_inductive Tm avoids
+lemma var_strengthen_aux:
+  shows "\<Delta> \<turnstile> \<Gamma>' @ BVar x \<tau> # \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<Gamma>' @ \<Gamma>"
+  and "\<Gamma>' @ BVar x \<tau> # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k \<longrightarrow> \<Gamma>' @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k"
+proof (induction rule: Ctx_Ty_induct_split)
+  case Ctx_Empty
+  then show ?case using context_valid(1) by auto
+next
+  case (Ctx_TyVar \<Gamma>' b k2)
+  then show ?case by (metis Ctx.simps append_Cons fresh_Cons fresh_append)
+next
+  case (Ctx_Var \<Gamma>' \<tau> x)
+  then have "atom x \<sharp> \<Gamma>' @ \<Gamma>" using fresh_append fresh_Cons by blast
+  then show ?case using Ctx_intros(3)[OF Ctx_Var(2)] by simp
+next
+  case (Ty_Var \<Gamma>' b k2)
+  then have "BTyVar b k2 \<in> (\<Gamma>' @ \<Gamma>)" using strengthen_isin_tyvar by simp
+  then show ?case by (rule Ty_intros(1)[OF Ty_Var(2)])
+qed (auto intro: Ty_intros)
+lemma var_strengthen_context: "\<Delta> \<turnstile> \<Gamma>' @ BVar x \<tau> # \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>' @ \<Gamma>"
+  using var_strengthen_aux by simp
+lemma var_strengthen_ty: "\<Gamma>' @ BVar x \<tau> # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k \<Longrightarrow> \<Gamma>' @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k"
+  using var_strengthen_aux by simp
+lemmas strengthen = var_strengthen_context var_strengthen_ty
+
+lemma context_cons_valid[elim]: "(\<Delta>::\<Delta>) \<turnstile> bndr # \<Gamma> \<Longrightarrow> (\<Delta> \<turnstile> \<Gamma> \<Longrightarrow> P) \<Longrightarrow> P"
+  by (cases rule: Ctx.cases) (auto simp: context_valid(1))
+
+lemma isin_subset:
+  fixes \<Gamma>::"\<Gamma>"
+  assumes "\<Delta> \<turnstile> \<Gamma>' @ \<Gamma>"
+  shows "bndr \<in> \<Gamma> \<longrightarrow> bndr \<in> (\<Gamma>' @ \<Gamma>)"
+proof
+  assume "bndr \<in> \<Gamma>"
+  then show "bndr \<in> (\<Gamma>' @ \<Gamma>)"
+  using assms proof (induction \<Gamma>' arbitrary: \<Gamma>)
+    case (Cons b \<Gamma>2)
+    have 1: "\<Delta> \<turnstile> \<Gamma>2 @ \<Gamma>" using Cons(3) by auto
+    have 2: "bndr \<in> (\<Gamma>2 @ \<Gamma>)" by (rule Cons(1)[OF Cons(2) 1])
+    show ?case
+    proof (cases b rule: binder.exhaust)
+      case (BVar x \<tau>)
+      then have "atom x \<sharp> (\<Gamma>2 @ \<Gamma>)" using Cons by auto
+      then show ?thesis using 2 BVar fresh_not_isin_var by (cases bndr rule: binder.exhaust) auto
+    next
+      case (BTyVar a k)
+      then have "atom a \<sharp> (\<Gamma>2 @ \<Gamma>)" using Cons by auto
+      then show ?thesis using 2 BTyVar fresh_not_isin_tyvar by (cases bndr rule: binder.exhaust) auto
+    qed
+  qed auto
+qed
+
+lemma Ty_Forall_Inv:
+  assumes a: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y (\<forall>a:k. \<sigma>) : \<tau>" and b: "atom a \<sharp> \<Gamma>"
+  shows "BTyVar a k # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star> \<and> \<tau> = \<star>"
+proof (cases rule: Ty.cases[OF a])
+  case (5 a' k' \<Gamma>' \<Delta>' \<sigma>')
+  then have 1: "(BTyVar a' k # \<Gamma>) , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma>' : \<star>" by simp
+  have valid: "\<turnstile> \<Delta>" by (rule axioms_valid(2)[OF 1])
+  have "(a' \<leftrightarrow> a) \<bullet> \<sigma>' = \<sigma>" using Abs_rename_body[of a' \<sigma>' a \<sigma>] 5(3) by auto
+  then have 2: "((a' \<leftrightarrow> a) \<bullet> (BTyVar a' k # \<Gamma>)) , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star>" using Ty.eqvt[OF 1, of "(a' \<leftrightarrow> a)"] valid by auto
+  have 3: "((a' \<leftrightarrow> a) \<bullet> (BTyVar a' k # \<Gamma>)) = BTyVar a k # ((a' \<leftrightarrow> a) \<bullet> \<Gamma>)" using Cons_eqvt flip_fresh_fresh by force
+  have 4: "(a' \<leftrightarrow> a) \<bullet> \<Gamma> = \<Gamma>" by (metis 5(1,5) CtxE(1) b context_valid_ty flip_def swap_fresh_fresh)
+  show ?thesis using 2 3 4 5(4) by argo
+qed simp_all
+
+lemma weaken_isin: "\<lbrakk> bndr \<in> (\<Gamma> @ \<Gamma>') ; \<Delta> \<turnstile> \<Gamma> @ xs @ \<Gamma>' \<rbrakk> \<Longrightarrow> bndr \<in> (\<Gamma> @ xs @ \<Gamma>')"
+proof (induction \<Gamma> arbitrary: bndr \<Gamma>' xs)
+  case Nil
+  then show ?case by (cases bndr rule: binder.exhaust) (auto simp: isin_subset)
+next
+  case (Cons b \<Gamma>)
+  have 1: "\<Delta> \<turnstile> \<Gamma> @ xs @ \<Gamma>'" using Cons(3) Ctx.cases by auto
+  then show ?case
+  proof (cases b rule: binder.exhaust)
+    case (BVar x \<tau>)
+    then show ?thesis using 1 Cons by (cases bndr rule: binder.exhaust) auto
+  next
+    case (BTyVar a k)
+    then show ?thesis using 1 Cons by (cases bndr rule: binder.exhaust) auto
+  qed
+qed
+
+lemma weaken_ty: "\<lbrakk> \<Gamma> @ \<Gamma>' , \<Delta>  \<turnstile>\<^sub>t\<^sub>y \<tau> : k ; \<Delta> \<turnstile> \<Gamma> @ xs @ \<Gamma>' \<rbrakk> \<Longrightarrow> \<Gamma> @ xs @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k"
+proof (nominal_induct \<tau> avoiding: \<Gamma> \<Gamma>' xs k rule: \<tau>.strong_induct)
+  case (TyVar x)
+  have 1: "BTyVar x k \<in> (\<Gamma> @ \<Gamma>')" by (cases rule: Ty.cases[OF TyVar(1)]) auto
+  show ?case by (rule Ty_Var[OF TyVar(2) weaken_isin[OF 1 TyVar(2)]])
+next
+  case (TyData T)
+  then have "AxData T k \<in> set \<Delta>" by blast
+  then show ?case by (rule Ty_Data[OF TyData(2)])
+next
+  case TyArrow
+  then have "k = (\<star> \<rightarrow> \<star> \<rightarrow> \<star>)" by blast
+  then show ?case using Ty_Arrow[OF TyArrow(2)] by argo
+next
+  case (TyApp \<tau>1 \<tau>2)
+  then obtain k1 where P: "\<Gamma> @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>1 : k1 \<rightarrow> k" "\<Gamma> @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>2 : k1" by blast
+  have 2: "\<Gamma> @ xs @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>1 : k1 \<rightarrow> k" by (rule TyApp(1)[OF P(1) TyApp(4)])
+  have 3: "\<Gamma> @ xs @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>2 : k1" by (rule TyApp(2)[OF P(2) TyApp(4)])
+  show ?case by (rule Ty_App[OF 2 3])
+next
+  case (TyForall a k1 \<sigma>)
+  have P: "(BTyVar a k1 # \<Gamma>) @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star>" "k = \<star>" using Ty_Forall_Inv[OF TyForall(6)] TyForall(1,2) fresh_append by auto
+  have 1: "atom a \<sharp> \<Gamma> @ xs @ \<Gamma>'" using TyForall(1-3) fresh_append by blast
+  have 2: "\<Delta> \<turnstile> (BTyVar a k1 # \<Gamma>) @ xs @ \<Gamma>'" using Ctx_TyVar[OF TyForall(7) 1] by simp
+  have 3: "BTyVar a k1 # \<Gamma> @ xs @ \<Gamma>' , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star>" using TyForall(5)[OF P(1) 2] by simp
+  show ?case using Ty_Forall[OF 3] P(2) by simp
+qed
+
+lemma weaken_axioms_ty: "\<lbrakk> \<Gamma> , \<Delta>' @ \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k ; \<Delta>' @ xs @ \<Delta> \<turnstile> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> ,  \<Delta>' @ xs @ \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k"
+proof (nominal_induct \<tau> avoiding: \<Delta> \<Delta>' k xs \<Gamma> rule: \<tau>.strong_induct)
+  case (TyApp \<tau>1 \<tau>2)
+  then show ?case using Ty_App by blast
+next
+  case (TyForall a k1 \<sigma>)
+  have P: "BTyVar a k1 # \<Gamma> , \<Delta>' @ \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star>" "k = \<star>" using Ty_Forall_Inv[OF TyForall(7,5)] by auto
+  have 1: "BTyVar a k1 # \<Gamma> , \<Delta>' @ xs @ \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : \<star>" by (rule TyForall(6)[OF P(1) Ctx_TyVar[OF TyForall(8,5)]])
+  show ?case using Ty_Forall[OF 1] P(2) by argo
+qed (auto intro: Ty_intros)
+lemmas weaken = weaken_isin weaken_ty weaken_axioms_ty
+
+(* inversion rules for abstractions *)
+lemma T_Abs_Inv:
+  assumes a: "\<Gamma> , \<Delta> \<turnstile> (\<lambda>x : \<tau>1 . e) : \<tau>" and b: "atom x \<sharp> \<Gamma>"
+  obtains \<tau>2 where "BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e : \<tau>2" "\<tau> = arrow_app \<tau>1 \<tau>2"
+proof (cases rule: Tm.cases[OF a])
+  case (2 x' \<tau>1' \<Gamma>' \<Delta>' e' \<tau>2)
+  then have swap: "(x' \<leftrightarrow> x) \<bullet> e' = e" using Abs_rename_body[of x' e' x e] by auto
+  have valid: "\<turnstile> \<Delta>" using axioms_valid(3)[OF 2(5)] 2(2) by simp
+  show ?thesis
+  proof (cases "atom x' = atom x")
+    case True
+    then show ?thesis using 2 swap that by auto
+  next
+    case False
+    then have 1: "atom x \<sharp> BVar x' \<tau>1' # \<Gamma>'" using b by (simp add: 2 fresh_Cons)
+    have 3: "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1 # \<Gamma>)) , \<Delta> \<turnstile> (x' \<leftrightarrow> x) \<bullet> e' : \<tau>2" using 2 Tm.eqvt[OF 2(5), of "(x' \<leftrightarrow> x)"] by fastforce
+    have "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1) # ((x' \<leftrightarrow> x) \<bullet> \<Gamma>)) = BVar x \<tau>1 # \<Gamma>"
+      by (metis "1" "2"(1) "2"(5) CtxE(2) binder.perm_simps(1) context_valid_tm flip_at_simps(1) flip_fresh_fresh fresh_Cons perm_\<tau>_vars)
+    then show ?thesis using 1 2 3 swap that by auto
+  qed
+qed simp_all
+
+lemma T_Let_Inv:
+  assumes a: "\<Gamma> , \<Delta> \<turnstile> Let x \<tau>1 e1 e2 : \<tau>" and b: "atom x \<sharp> \<Gamma>"
+  shows "\<Gamma> , \<Delta> \<turnstile> e1 : \<tau>1 \<and> BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e2 : \<tau>"
+proof (cases rule: Tm.cases[OF a])
+  case (7 \<Gamma>' \<Delta>' e1' \<tau>1' x' e2' \<tau>2')
+  have swap: "(x' \<leftrightarrow> x) \<bullet> e2' = e2" using Abs_rename_body[of x' e2' x e2] 7(3) by simp
+  show ?thesis
+  proof (cases "atom x' = atom x")
+    case True
+    then show ?thesis using 7 swap by auto
+  next
+    case False
+    then have 1: "atom x \<sharp> BVar x' \<tau>1 # \<Gamma>'" using b by (simp add: 7 fresh_Cons)
+    have 2: "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1#\<Gamma>)) , \<Delta> \<turnstile> (x' \<leftrightarrow> x) \<bullet> e2' : \<tau>" using Tm.eqvt[OF 7(6), of "(x' \<leftrightarrow> x)"] 7 by auto
+    have 3: "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1) # ((x' \<leftrightarrow> x) \<bullet> \<Gamma>)) = BVar x \<tau>1#\<Gamma>"
+      by (metis "1" 7(1,6) CtxE(2) binder.perm_simps(1) context_valid_tm flip_at_simps(1) flip_def fresh_Cons perm_\<tau>_vars swap_fresh_fresh)
+    from 2 3 7 swap show ?thesis by auto
+  qed
+qed simp_all
+
+lemma T_AbsT_Inv:
+  assumes a: "\<Gamma> , \<Delta> \<turnstile> (\<Lambda> a : k . e) : \<tau>" and b: "atom a \<sharp> \<Gamma>" "atom a \<sharp> \<tau>"
+  obtains \<sigma> where "BTyVar a k # \<Gamma> , \<Delta> \<turnstile> e : \<sigma>" "\<tau> = (\<forall> a:k. \<sigma>)"
+proof (cases rule: Tm.cases[OF a])
+  case (4 a' k' \<Gamma>' \<Delta>' e' \<sigma>')
+  then have fresh: "atom a' \<sharp> \<Gamma>" by (cases rule: Ctx.cases[OF context_valid(2)[OF 4(5)]]) auto
+  have swap: "(a' \<leftrightarrow> a) \<bullet> e' = e" using Abs_rename_body[of a' e' a e] 4(3) by simp
+  have valid: "\<turnstile> \<Delta>" using axioms_valid(3)[OF 4(5)] 4(2) by simp
+  show ?thesis
+  proof (cases "atom a = atom a'")
+    case True
+    then show ?thesis by (metis 4 Abs1_eq_iff(3) atom_eq_iff term_alt_list_alt.eq_iff(6) that)
+  next
+    case False
+    then have 1: "atom a \<sharp> BTyVar a' k # \<Gamma>" using b by (simp add: 4 fresh_Cons)
+    have 2: "((a' \<leftrightarrow> a) \<bullet> (BTyVar a' k # \<Gamma>)), \<Delta> \<turnstile> (a' \<leftrightarrow> a) \<bullet> e' : (a' \<leftrightarrow> a) \<bullet> \<sigma>'" using Tm.eqvt[OF 4(5), of "(a' \<leftrightarrow> a)"] valid 4 by auto
+    have "((a' \<leftrightarrow> a) \<bullet> (BTyVar a' k # \<Gamma>)) = ((a' \<leftrightarrow> a) \<bullet> BTyVar a' k) # \<Gamma>" using 1 fresh flip_fresh_fresh b(1) by simp
+    then have "((a' \<leftrightarrow> a) \<bullet> (BTyVar a' k # \<Gamma>)) = BTyVar a k # \<Gamma>" by (simp add: flip_fresh_fresh)
+    then have "BTyVar a k # \<Gamma> , \<Delta> \<turnstile> e : (a' \<leftrightarrow> a) \<bullet> \<sigma>'" using 2 swap by argo
+    then show ?thesis by (metis "4"(3,4) Abs1_eq_iff(3) False \<tau>.eq_iff(5) \<tau>.fresh(5) b(2) empty_iff flip_commute insert_iff list.set(1,2) term_alt_list_alt.eq_iff(6) that)
+  qed
+qed simp_all
+
+lemma zip_with_context_fresh_vars: "\<lbrakk> \<Delta> \<turnstile> zip_with BVar vars xs @ \<Gamma> ; length vars \<le> length xs \<rbrakk> \<Longrightarrow> set (map atom vars) \<sharp>* \<Gamma>"
+proof (induction vars arbitrary: xs)
+  case Nil
+  then show ?case using fresh_star_def by auto
+next
+  case (Cons a vars)
+  then obtain x xs' where P: "xs = x # xs'" by (cases xs) auto
+  then have 1: "length vars \<le> length xs'" using Cons by simp
+  let ?\<Gamma> = "zip_with BVar vars xs' @ \<Gamma>"
+  from P have "\<Delta> \<turnstile> BVar a x # ?\<Gamma>" using Cons(2) by simp
+  then have "?\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y x : \<star>" and 2:"atom a \<sharp> ?\<Gamma>" by auto
+  then have 3: "\<Delta> \<turnstile> ?\<Gamma>" using context_valid(1) by simp
+  show ?case using Cons(1)[OF 3 1] 2 fresh_append
+    by (metis (no_types, lifting) fresh_star_def list.simps(9) set_ConsD)
+qed
+
+lemma zip_with_context_fresh_tyvars: "\<lbrakk> \<Delta> \<turnstile> zip_with BTyVar tys xs @ \<Gamma> ; length tys \<le> length xs \<rbrakk> \<Longrightarrow> set (map atom tys) \<sharp>* \<Gamma>"
+proof (induction tys arbitrary: xs)
+  case Nil
+  then show ?case using fresh_star_def by auto
+next
+  case (Cons a vars)
+  then obtain x xs' where P: "xs = x # xs'" by (cases xs) auto
+  then have 1: "length vars \<le> length xs'" using Cons by simp
+  let ?\<Gamma> = "zip_with BTyVar vars xs' @ \<Gamma>"
+  from P have "\<Delta> \<turnstile> BTyVar a x # ?\<Gamma>" using Cons(2) by simp
+  then have 3: "\<Delta> \<turnstile> ?\<Gamma>" "atom a \<sharp> ?\<Gamma>" by auto
+  show ?case using Cons(1)[OF 3(1) 1] 3(2) fresh_append
+    by (metis (no_types, lifting) fresh_star_def list.simps(9) set_ConsD)
+qed
+
+lemma context_valid_append: "\<Delta>::\<Delta> \<turnstile> \<Gamma>' @ \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>"
+proof (induction \<Gamma>')
+  case (Cons a \<Gamma>')
+  then show ?case using context_valid(1) by (cases a rule: binder.exhaust) auto
+qed auto
+
+lemma axioms_split_valid: "\<turnstile> \<Delta>' @ \<Delta> \<Longrightarrow> \<turnstile> \<Delta>"
+proof (induction \<Delta>')
+  case (Cons a \<Delta>')
+  then show ?case using axioms_valid(2) by (cases a rule: axiom.exhaust) auto
+qed simp
+
+lemma axioms_regularity: "\<turnstile> \<Delta>' @ AxCtor D \<tau> # \<Delta> \<Longrightarrow> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>"
+  using Ax_Ctor axioms_split_valid by (induction \<Delta>) blast+
+
+lemma context_regularity: "\<Delta> \<turnstile> \<Gamma>' @ BVar x \<tau> # \<Gamma> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>"
+  using Ctx_Var context_valid_append by (induction \<Gamma>) blast+
+
+lemma isin_same_kind: "\<lbrakk> BTyVar a k1 \<in> (\<Gamma>' @ BTyVar a k2 # \<Gamma>) ; \<Delta> \<turnstile> \<Gamma>' @ BTyVar a k2 # \<Gamma> \<rbrakk> \<Longrightarrow> k1 = k2"
+proof (induction \<Gamma>')
+  case (Cons bndr \<Gamma>')
+  then show ?case by (cases rule: Ctx.cases[OF Cons(3)]) (auto split: if_splits simp: fresh_Cons fresh_append fresh_at_base(2))
+qed auto
+
+lemma isin_same_type: "\<lbrakk> BVar x \<tau> \<in> (\<Gamma>' @ BVar x \<tau>2 # \<Gamma>) ; \<Delta> \<turnstile> \<Gamma>' @ BVar x \<tau>2 # \<Gamma> \<rbrakk> \<Longrightarrow> \<tau> = \<tau>2"
+proof (induction \<Gamma>')
+  case (Cons a \<Gamma>')
+  then show ?case by (cases rule: Ctx.cases[OF Cons(3)]) (auto split: if_splits simp: fresh_Cons fresh_append fresh_at_base)
+qed auto
+lemmas isin_same = isin_same_kind isin_same_type
+
+lemma isin_subst_tyvar: "\<lbrakk> BTyVar a k \<in> (\<Gamma>' @ BTyVar b k2 # \<Gamma>) ; \<Delta> \<turnstile> \<Gamma>' @ BTyVar b k2 # \<Gamma> ; a \<noteq> b \<rbrakk> \<Longrightarrow> BTyVar a k \<in> (\<Gamma>'[\<sigma>/b] @ \<Gamma>)"
+proof (induction \<Gamma>')
+  case (Cons bndr \<Gamma>')
+  then show ?case
+  proof (cases rule: Ctx.cases[OF Cons(3)])
+    case (2 \<Gamma>2 c k3)
+    then have "BTyVar a k = bndr \<or> BTyVar a k \<in> (\<Gamma>' @ BTyVar b k2 # \<Gamma>)" by (metis Cons.prems(1) Cons_eq_append_conv isin.simps(5) list.inject)
+    then show ?thesis
+    proof
+      assume a: "BTyVar a k = bndr"
+      then show ?thesis using 2 Cons by auto
+    next
+      assume "BTyVar a k \<in> (\<Gamma>' @ BTyVar b k2 # \<Gamma>)"
+      then show ?thesis using 2 Cons fresh_not_isin_tyvar by auto
+    qed
+  next
+    case (3 \<Gamma> \<tau> x)
+    then show ?thesis using Cons by auto
+  qed simp
+qed simp
+
+lemma axiom_isin_split: "\<lbrakk> b \<in> set \<Delta> ; \<turnstile> \<Delta> \<rbrakk> \<Longrightarrow> \<exists>\<Delta>1 \<Delta>2. \<Delta> = \<Delta>1 @ b # \<Delta>2"
+proof (induction \<Delta>)
+  case (Cons a \<Delta>)
+  then show ?case
+  proof (cases "a = b")
+    case True
+    then show ?thesis by blast
+  next
+    case False
+    then show ?thesis by (meson Cons.prems(1) split_list)
+  qed
+qed simp
+
+lemma type_substitution_aux:
+  assumes "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k"
+  shows "(\<Delta> \<turnstile> (\<Gamma>' @ BTyVar a k # \<Gamma>) \<longrightarrow> \<Delta> \<turnstile> (subst_context \<Gamma>' \<sigma> a @ \<Gamma>))"
+    and "(\<Gamma>' @ BTyVar a k # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<longrightarrow> subst_context \<Gamma>' \<sigma> a @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y subst_type \<tau> \<sigma> a : k2)"
+proof (induction rule: Ctx_Ty_induct_split)
+  case Ctx_Empty
+  then show ?case using context_valid(1)[OF assms] by simp
+next
+  case (Ctx_TyVar \<Gamma>' b k2)
+  then have "atom b \<sharp> \<sigma>" using assms fresh_Cons fresh_append fresh_in_context_ty by blast
+  then have 1: "atom b \<sharp> \<Gamma>'[\<sigma>/a] @ \<Gamma>" by (meson Ctx_TyVar(3) fresh_Cons fresh_append fresh_subst_context_tyvar)
+  show ?case using Ax_Ctx_Ty.Ctx_TyVar[OF Ctx_TyVar(2) 1] assms by auto
+next
+  case (Ctx_Var \<Gamma>' \<tau> x)
+  have 1: "atom x \<sharp> \<Gamma>'[\<sigma>/a] @ \<Gamma>" by (meson Ctx_Var(3) fresh_Cons fresh_append fresh_subst_context_var)
+  show ?case using Ax_Ctx_Ty.Ctx_Var[OF Ctx_Var(2) 1] by simp
+next
+  case (Ty_Var \<Gamma>' b k2)
+  then show ?case
+    proof (cases "b = a")
+    case True
+    then have "k = k2" using isin_same(1) Ty_Var by blast
+    then have "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y (TyVar b)[\<sigma>/a] : k2" using True assms(1) by simp
+    then show ?thesis using weaken_ty[of "[]"] Ty_Var(2) by auto
+  next
+    case False
+    have 1: "BTyVar b k2 \<in> (\<Gamma>'[\<sigma>/a] @ \<Gamma>)" by (rule isin_subst_tyvar[OF Ty_Var(3,1) False])
+    show ?thesis using Ax_Ctx_Ty.Ty_Var[OF Ty_Var(2) 1] False by simp
+  qed
+next
+  case (Ty_Forall \<Gamma>' b k2 \<sigma>')
+  have 1: "a \<noteq> b" by (metis CtxE(1) Ty_Forall(1) binder.fresh(2) context_valid_ty fresh_Cons fresh_append fresh_at_base(2))
+  then have 2: "BTyVar b k2 # \<Gamma>'[\<sigma>/a] @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma>'[\<sigma>/a] : \<star>" using Ty_Forall(2) by simp
+  show "\<Gamma>'[\<sigma>/a] @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y (\<forall> b : k2 . \<sigma>')[\<sigma>/a] : \<star>" using Ax_Ctx_Ty.Ty_Forall[OF 2]
+    by (metis "1" "2" CtxE(1) assms atom_eq_iff context_valid_ty fresh_Pair fresh_append fresh_at_base(2) fresh_in_context_ty subst_type.simps(5))
+qed (auto intro: Ty_intros)
+corollary type_substitution_context: "\<lbrakk> \<Delta> \<turnstile> \<Gamma>' @ BTyVar a k # \<Gamma> ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>'[\<sigma>/a] @ \<Gamma>"
+  using type_substitution_aux by blast
+corollary type_substitution_ty: "\<lbrakk> \<Gamma>' @ BTyVar a k # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma> : k \<rbrakk> \<Longrightarrow> \<Gamma>'[\<sigma>/a] @ \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>[\<sigma>/a] : k2"
+  using type_substitution_aux by blast
+
+lemma typing_regularity: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>"
+proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct)
+  case (Tm_Var \<Delta> \<Gamma> x \<tau>)
+  then obtain \<Gamma>1 \<Gamma>2 where 1: "\<Gamma> = \<Gamma>1 @ BVar x \<tau> # \<Gamma>2" using isin_split by blast
+  then have "\<Gamma>2 , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>" using context_regularity Tm_Var(1) by blast
+  then show ?case using weaken_ty[of "[]" \<Gamma>2 \<Delta> \<tau> \<star> "\<Gamma>1 @ [BVar x \<tau>]"] Tm_Var(1) 1 by simp
+next
+  case (Tm_Abs x \<tau>1 \<Gamma> \<Delta> e \<tau>2)
+  have 1: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>1 : \<star>" using context_regularity context_valid(1)[OF Tm_Abs(2)] by blast
+  have 2: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>2 : \<star>" using strengthen(2)[of "[]"] Tm_Abs(2) by force
+  have 3: "\<Delta> \<turnstile> \<Gamma>" by (rule context_valid(1)[OF 1])
+  show ?case by (rule Ty_App[OF Ty_App[OF Ty_Arrow[OF 3] 1] 2])
+next
+  case (Tm_TApp \<Gamma> \<Delta> e a k \<sigma> \<tau>)
+  obtain a' \<sigma>' where P: "(\<forall> a:k. \<sigma>) = (\<forall> a':k. \<sigma>')" "BTyVar a' k # \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma>' : \<star>" by (cases rule: Ty.cases[OF Tm_TApp(3)]) auto
+  have "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<sigma>'[\<tau>/a'] : \<star>" using type_substitution_ty[of "[]", OF _ Tm_TApp(2)] P by auto
+  then show ?case using P(1) subst_type_same by auto
+next
+  case (Tm_Ctor \<Delta> \<Gamma> D \<tau>)
+  from Tm_Ctor(1) have 1: "\<turnstile> \<Delta>" by (rule axioms_valid(1))
+  then obtain \<Delta>1 \<Delta>2 where 2: "\<Delta> = \<Delta>1 @ AxCtor D \<tau> # \<Delta>2" using axiom_isin_split[OF Tm_Ctor(2) 1] by blast
+  then have "[] , \<Delta>2 \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>" using axioms_regularity 1 by blast
+  then have "[] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star>" using weaken(3)[of "[]" "[]" \<Delta>2 \<tau> \<star> "\<Delta>1 @ [AxCtor D \<tau>]"] 1 2 Ctx_Empty by simp
+  then show ?case using weaken(2)[of "[]" "[]"] Tm_Ctor(1) by simp
+next
+  case (Tm_Let \<Gamma> \<Delta> e1 \<tau>1 x e2 \<tau>2)
+  then show ?case using strengthen(2)[of "[]"] by force
+qed (auto intro: Ty_intros)
+
+corollary supp_cty: "\<lbrakk> \<turnstile> \<Delta> ; AxCtor K cty \<in> set \<Delta> \<rbrakk> \<Longrightarrow> supp cty = {}"
+  using axioms_empty_supp by (metis axiom.supp(2) axioms_split_valid split_list sup_bot.neutr_eq_iff supp_Cons) 
+
+lemma supp_args:
+  assumes "\<Gamma> , \<Delta> \<turnstile> e : \<tau>1" "head_data \<tau>1 = Some (T, \<sigma>s)" "AxCtor K cty \<in> set \<Delta>" "subst_ctor cty \<sigma>s = Some args"
+  shows "supp args \<subseteq> supp \<Gamma>"
+proof -
+  have 1: "supp cty = {}" by (rule supp_cty[OF axioms_valid(3)[OF assms(1)] assms(3)])
+  have "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau>1 : \<star>" by (rule typing_regularity[OF assms(1)])
+  then have "supp \<tau>1 \<subseteq> supp \<Gamma>" by (rule supp_in_context_ty)
+  then have "supp \<sigma>s \<subseteq> supp \<Gamma>" using supp_head_data[OF assms(2)] by simp
+  then show "supp args \<subseteq> supp \<Gamma>" using supp_subst_ctor[OF assms(4)] 1 by simp
+qed
+
+corollary supp_in_context_term_type: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longrightarrow> supp \<tau> \<subseteq> supp \<Gamma>"
+  using supp_in_context_ty[OF typing_regularity] by simp
+
+lemma supp_in_context_term: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longrightarrow> supp e \<subseteq> supp \<Gamma>"
+proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct)
+  case (Tm_Var \<Delta> \<Gamma> x \<tau>)
+  then show ?case by (metis fresh_def fresh_not_isin_var singletonD subsetCI supp_at_base term_alt_list_alt.supp(1))
+next
+  case (Tm_Abs x \<tau>1 \<Gamma> \<Delta> e \<tau>2)
+  then have "supp \<tau>1 \<subseteq> supp \<Gamma>" by (meson CtxE(2) context_valid_tm supp_in_context_ty) 
+  then show ?case using Tm_Abs(2) unfolding supp_Cons binder.supp supp_at_base term_supp by auto
+next
+  case (Tm_App \<Gamma> \<Delta> e1 \<tau>1 \<tau>2 e2)
+  then show ?case unfolding term_supp by simp
+next
+  case (Tm_TAbs a k \<Gamma> \<Delta> e \<sigma>)
+  then show ?case unfolding supp_Cons binder.supp pure_supp term_supp supp_at_base by auto
+next
+  case (Tm_TApp \<Gamma> \<Delta> e a k \<sigma> \<tau>)
+  then have "supp \<tau> \<subseteq> supp \<Gamma>" using supp_in_context_ty by simp
+  then show ?case using Tm_TApp(3) unfolding term_supp by auto
+next
+  case (Tm_Ctor \<Delta> \<Gamma> D \<tau>)
+  then show ?case unfolding term_supp pure_supp by simp
+next
+  case (Tm_Let \<Gamma> \<Delta> e1 \<tau>1 x e2 \<tau>2)
+  then have "supp \<tau>1 \<subseteq> supp \<Gamma>" using supp_in_context_term_type by auto
+  then show ?case using Tm_Let(3,4) unfolding term_supp supp_Cons binder.supp supp_at_base by auto
+next
+  case (Tm_Case \<Gamma> \<Delta> e \<tau>1 T \<sigma>s \<tau> alts)
+  have "\<forall>alt |\<in>| set_alts alts. supp alt \<subseteq> supp \<Gamma>" using Tm_Case(6)
+  proof (induction rule: alts_induct)
+    case (MatchCtor K tys vals e' cty ks args)
+    have "supp args \<subseteq> supp \<Gamma>" by (rule supp_args[OF Tm_Case(1,2) MatchCtor(1,3)])
+    then have "supp e' \<subseteq> supp tys \<union> supp vals \<union> supp \<Gamma>" using supp_zip_with MatchCtor(5) unfolding supp_append by fastforce
+    then show ?case unfolding alt_supp pure_supp using supp_vars supp_tyvars by auto
+  qed
+  then have "supp alts \<subseteq> supp \<Gamma>"
+    by (induction alts rule: term_alt_list_alt.inducts(2)) (auto simp: alt_list_supp)
+  then show ?case using Tm_Case term_supp by auto
+qed
+lemmas supp_in_context = supp_in_context_ty supp_in_context_term supp_in_context_term_type
+
+corollary fresh_in_context_term_var: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (y::var) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom y \<sharp> e"
+  using supp_in_context_term unfolding fresh_def by blast
+corollary fresh_in_context_term_tyvar: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> e"
+  using supp_in_context_term unfolding fresh_def by blast
+corollary fresh_in_context_term_type_tyvar: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> \<tau>"
+  using supp_in_context_term_type unfolding fresh_def by blast
+lemmas fresh_in_context = fresh_in_context_ty fresh_in_context_term_var fresh_in_context_term_tyvar fresh_in_context_term_type_tyvar
+
+(*nominal_inductive Tm avoids
   Tm_Abs: x
   | Tm_TAbs: a
   | Tm_Let: x
@@ -259,6 +711,6 @@ next
   then obtain y e2' where 2: "Let x \<tau>1 e1 e2 = Let y \<tau>1 e1 e2' \<and> atom x \<sharp> Let y \<tau>1 e1 e2'" using Abs_fresh_var by auto
   then have "atom x \<sharp> (\<Gamma>, \<Delta>, Let y \<tau>1 e1 e2', \<tau>2)" using 1 fresh_Pair by simp
   then show ?case using 2 fresh_star_def by fastforce
-qed auto
+qed auto*)
 
 end