[STATEMENT]
lemma typings_append: 
  assumes "CT;\<Gamma> \<turnstile>+ es : Cs"
  and "CT;\<Gamma> \<turnstile> e : C"
  shows "CT;\<Gamma> \<turnstile>+ (es@[e]) : (Cs@[C])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
have "length es = length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length es = length Cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. length es = length Cs
[PROOF STEP]
by(simp_all add:typings_lengths)
[PROOF STATE]
proof (state)
this:
length es = length Cs

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
thus "CT;\<Gamma> \<turnstile>+ (es@[e]) : (Cs@[C])"
[PROOF STATE]
proof (prove)
using this:
length es = length Cs

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length es = length Cs
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])
[PROOF STEP]
proof(induct "es" "Cs" rule:list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ []:[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ [] : []
[PROOF STEP]
by(simp add:typings_typing.ts_nil)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ [] : []

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ [] : []

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
have "CT;\<Gamma> \<turnstile> e : C"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ es : Cs
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile> e : C

goal (2 subgoals):
 1. \<lbrakk>CT;\<Gamma> \<turnstile>+ [] : []; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ [] : []
CT;\<Gamma> \<turnstile> e : C
[PROOF STEP]
show "CT;\<Gamma> \<turnstile>+ ([]@[e]) : ([]@[C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ [] : []
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])
[PROOF STEP]
by (auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ([] @ [e]) : ([] @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
fix x xs y ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
assume "length xs = length ys" 
      and IH: "\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])"
      and x_xs_typs: "CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)"
      and e_typ: "CT;\<Gamma> \<turnstile> e : C"
[PROOF STATE]
proof (state)
this:
length xs = length ys
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)
CT;\<Gamma> \<turnstile> e : C

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
from x_xs_typs
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)
[PROOF STEP]
have x_typ: "CT;\<Gamma> \<turnstile> x : y" and "CT;\<Gamma> \<turnstile>+ xs : ys"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys)

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile> x : y &&& CT;\<Gamma> \<turnstile>+ xs : ys
[PROOF STEP]
by(auto elim:typings.cases)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
with IH e_typ
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile> e : C
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ (xs@[e]) : (ys@[C])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
CT;\<Gamma> \<turnstile> e : C
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ xs : ys

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
with x_typ
[PROOF STATE]
proof (chain)
picking this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])
[PROOF STEP]
have "CT;\<Gamma> \<turnstile>+ ((x#xs)@[e]) : ((y#ys)@[C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile> x : y
CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C])

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
by (auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>CT;\<Gamma> \<turnstile>+ xs : ys; CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ (xs @ [e]) : (ys @ [C]); CT;\<Gamma> \<turnstile>+ (x # xs) : (y # ys); CT;\<Gamma> \<turnstile> e : C\<rbrakk> \<Longrightarrow> CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
thus "CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])"
[PROOF STATE]
proof (prove)
using this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal (1 subgoal):
 1. CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])
[PROOF STEP]
by(auto simp add:typings_typing.ts_cons)
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ ((x # xs) @ [e]) : ((y # ys) @ [C])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
CT;\<Gamma> \<turnstile>+ (es @ [e]) : (Cs @ [C])

goal:
No subgoals!
[PROOF STEP]
qed