You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inductive Term : Nat -> Nat -> Nat -> Type where
 
| var : Fin n -> Term n m k
 
| lam : CType n m k -> Term (n+1) m k -> Term n m k
 
| tlam : SType n m k -> Term n (m+1) k -> Term n m k
 
| clam : CBound n k -> Term n m (k+1) -> Term n m k
 
| pack : CaptureSet n k -> Fin n -> Term n m k
 
| app : Fin n -> Fin n -> Term n m k
 
| invoke : Fin n -> Fin n -> Term n m k
 
| tapp : Fin n -> Fin m -> Term n m k
 
| capp : Fin n -> Fin k -> Term n m k
 
| letin : Term n m k -> Term (n+1) m k -> Term n m k
 
| letex : Term n m k -> Term (n+1) m (k+1) -> Term n m k
 
| bindt : SType n m k -> Term n (m+1) k -> Term n m k
 
| bindc : CaptureSet n k -> Term n m (k+1) -> Term n m k
 
| boundary : SType n m k -> Term (n+1) m (k+1) -> Term n m k

@[aesop safe constructors]
inductive Term.IsValue : Term n m k -> Prop where
| lam : Term.IsValue (lam E t)
| tlam : Term.IsValue (tlam S t)
| clam : Term.IsValue (clam B t)
| pack : Term.IsValue (pack c x)

def Term.rename (t : Term n m k) (f : FinFun n n') : Term n' m k :=
  match t with
  | Term.var x => Term.var (f x)
  | Term.lam E t => Term.lam (E.rename f) (t.rename f.ext)
  | Term.tlam S t => Term.tlam (S.rename f) (t.rename f)
  | Term.clam B t => Term.clam (B.rename f) (t.rename f)
  | Term.pack C x => Term.pack (C.rename f) (f x)
  | Term.app x y => Term.app (f x) (f y)
  | Term.invoke x y => Term.invoke (f x) (f y)
  | Term.tapp x X => Term.tapp (f x) X
  | Term.capp x c => Term.capp (f x) c
  | Term.letin t u => Term.letin (t.rename f) (u.rename f.ext)
  | Term.letex t u => Term.letex (t.rename f) (u.rename f.ext)
  | Term.bindt S t => Term.bindt (S.rename f) (t.rename f)
  | Term.bindc c t => Term.bindc (c.rename f) (t.rename f)
  | Term.boundary S t => Term.boundary (S.rename f) (t.rename f.ext)

def Term.crename (t : Term n m k) (f : FinFun k k') : Term n m k' :=
  match t with
  | Term.var x => Term.var x
  | Term.lam E t => Term.lam (E.crename f) (t.crename f)
  | Term.tlam S t => Term.tlam (S.crename f) (t.crename f)
  | Term.clam B t => Term.clam (B.crename f) (t.crename f.ext)
  | Term.pack C x => Term.pack (C.crename f) x
  | Term.app x y => Term.app x y
  | Term.invoke x y => Term.invoke x y
  | Term.tapp x X => Term.tapp x X
  | Term.capp x c => Term.capp x (f c)
  | Term.letin t u => Term.letin (t.crename f) (u.crename f)
  | Term.letex t u => Term.letex (t.crename f) (u.crename f.ext)
  | Term.bindt S t => Term.bindt (S.crename f) (t.crename f)
  | Term.bindc c t => Term.bindc (c.crename f) (t.crename f.ext)
  | Term.boundary S t => Term.boundary (S.crename f) (t.crename f.ext)

def Term.weaken (t : Term n m k) : Term (n+1) m k := t.rename FinFun.weaken

def Term.weaken1 (t : Term (n+1) m k) : Term (n+2) m k :=
  t.rename FinFun.weaken.ext

def Term.cweaken (t : Term n m k) : Term n m (k+1) := t.crename FinFun.weaken

def Term.cweaken1 (t : Term n m (k+1)) : Term n m (k+2) :=
  t.crename FinFun.weaken.ext

inductive CaptureSet : Nat -> Nat -> Type where
| empty : CaptureSet n k
| union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k
| singleton : Fin n -> CaptureSet n k
| csingleton : Fin k -> CaptureSet n k

inductive CaptureSet.Subset : CaptureSet n k → CaptureSet n k → Prop where
| empty : Subset {} C
| rfl : Subset C C
| union_l :
  Subset C1 C ->
  Subset C2 C ->
  Subset (C1 ∪ C2) C
| union_rl :
  Subset C C1 ->
  Subset C (C1 ∪ C2)
| union_rr :
  Subset C C2 ->
  Subset C (C1 ∪ C2)

@[simp]
def CaptureSet.rename (C : CaptureSet n k) (f : FinFun n n') : CaptureSet n' k :=
  match C with
  | empty => empty
  | union C1 C2 => (C1.rename f) ∪ (C2.rename f)
  | singleton x => {x=f x}
  | csingleton c => {c=c}

@[simp]
def CaptureSet.crename (C : CaptureSet n k) (f : FinFun k k') : CaptureSet n k' :=
  match C with
  | empty => empty
  | union C1 C2 => (C1.crename f) ∪ (C2.crename f)
  | singleton x => {x=x}
  | csingleton c => {c=f c}

def CaptureSet.weaken (C : CaptureSet n k) : CaptureSet (n+1) k :=
  C.rename FinFun.weaken

def CaptureSet.weaken1 (C : CaptureSet (n+1) k) : CaptureSet (n+2) k :=
  C.rename FinFun.weaken.ext

def CaptureSet.cweaken (C : CaptureSet n k) : CaptureSet n (k+1) :=
  C.crename FinFun.weaken

def CaptureSet.cweaken1 (C : CaptureSet n (k+1)) : CaptureSet n (k+2) :=
  C.crename FinFun.weaken.ext

def FinFun (n n' : Nat) : Type :=
  Fin n -> Fin n'

def FinFun.weaken : FinFun n (n+1) :=
  Fin.succ

def FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) :=

inductive TBinding : Nat -> Nat -> Nat -> Type where
| bound : SType n m k -> TBinding n m k
| inst : SType n m k -> TBinding n m k

inductive CBinding : Nat -> Nat -> Type where
| bound : CBound n k -> CBinding n k
| inst : CaptureSet n k -> CBinding n k

inductive Context : Nat -> Nat -> Nat -> Type where
| empty : Context 0 0 0
| var : Context n m k -> CType n m k -> Context (n+1) m k
| label : Context n m k -> SType n m k -> Context (n+1) m k
| tvar : Context n m k -> TBinding n m k -> Context n (m+1) k
| cvar : Context n m k -> CBinding n k -> Context n m (k+1)

def TBinding.rename (b : TBinding n m k) (f : FinFun n n') : TBinding n' m k :=
  match b with
  | bound S => bound (S.rename f)
  | inst S => inst (S.rename f)

def TBinding.trename (b : TBinding n m k) (f : FinFun m m') : TBinding n m' k :=
  match b with
  | bound S => bound (S.trename f)
  | inst S => inst (S.trename f)

def TBinding.crename (b : TBinding n m k) (f : FinFun k k') : TBinding n m k' :=
  match b with
  | bound S => bound (S.crename f)
  | inst S => inst (S.crename f)

def CBinding.rename (b : CBinding n k) (f : FinFun n n') : CBinding n' k :=
  match b with
  | bound b0 => bound (b0.rename f)
  | inst C => inst (C.rename f)

def CBinding.crename (b : CBinding n k) (f : FinFun k k') : CBinding n k' :=
  match b with
  | bound b0 => bound (b0.crename f)
  | inst C => inst (C.crename f)

def TBinding.weaken (b : TBinding n m k) : TBinding (n+1) m k :=
  b.rename FinFun.weaken

def CBinding.weaken (b : CBinding n k) : CBinding (n+1) k :=
  b.rename FinFun.weaken

def TBinding.tweaken (b : TBinding n m k) : TBinding n (m+1) k :=
  b.trename FinFun.weaken

def TBinding.cweaken (b : TBinding n m k) : TBinding n m (k+1) :=
  b.crename FinFun.weaken

def CBinding.cweaken (b : CBinding n k) : CBinding n (k+1) :=
  b.crename FinFun.weaken

inductive Context.TBound : Context n m k -> Fin m -> TBinding n m k -> Prop where
| here : TBound (tvar Γ0 b) 0 b.tweaken
| there_var :
  TBound Γ x b ->
  TBound (var Γ E) x b.weaken
| there_tvar :
  TBound Γ x b ->
  TBound (tvar Γ b') (Fin.succ x) b.tweaken
| there_cvar :
  TBound Γ x b ->
  TBound (cvar Γ b') x b.cweaken
| there_label :
  TBound Γ x b ->
  TBound (label Γ S) x b.weaken

inductive Context.LBound : Context n m k -> Fin n -> SType n m k -> Prop where
| here : LBound (label Γ0 S) 0 S.weaken
| there_var :
  LBound Γ x S ->
  LBound (var Γ E) x.succ S.weaken
| there_tvar :
  LBound Γ x S ->
  LBound (tvar Γ b) x S.tweaken
| there_cvar :
  LBound Γ x S ->
  LBound (cvar Γ b) x S.cweaken
| there_label :
  LBound Γ x S ->
  LBound (label Γ S') x.succ S.weaken

inductive CBound : Nat -> Nat -> Type where
| upper : CaptureSet n k -> CBound n k
| star : CBound n k

inductive EType : Nat -> Nat -> Nat -> Type where
| ex : CType n m (k+1) -> EType n m k
| type : CType n m k -> EType n m k

inductive CType : Nat -> Nat -> Nat -> Type where
| capt : CaptureSet n k -> SType n m k -> CType n m k

inductive SType : Nat -> Nat -> Nat -> Type where
| top : SType n m k
| tvar : Fin m -> SType n m k
| forall : CType n m k -> EType (n+1) m k -> SType n m k
| tforall : SType n m k -> EType n (m+1) k -> SType n m k
| cforall : CBound n k -> EType n m (k+1) -> SType n m k
| box : CType n m k -> SType n m k
| label : SType n m k -> SType n m k

def CBound.rename (b : CBound n k) (f : FinFun n n') : CBound n' k :=
  match b with
  | upper C => upper (C.rename f)
  | star => star

def CBound.crename (b : CBound n k) (f : FinFun k k') : CBound n k' :=
  match b with
  | upper C => upper (C.crename f)
  | star => star

def CBound.weaken (b : CBound n k) : CBound (n+1) k :=
  b.rename FinFun.weaken

def CBound.cweaken (b : CBound n k) : CBound n (k+1) :=
  b.crename FinFun.weaken

def EType.rename : EType n m k -> FinFun n n' -> EType n' m k
| EType.ex T, f => EType.ex (T.rename f)
| EType.type T, f => EType.type (T.rename f)

def CType.rename : CType n m k -> FinFun n n' -> CType n' m k
| CType.capt C S, f => CType.capt (C.rename f) (S.rename f)

def SType.rename : SType n m k -> FinFun n n' -> SType n' m k
| SType.top, _ => SType.top
| SType.tvar X, _ => SType.tvar X
| SType.forall E1 E2, f => SType.forall (E1.rename f) (E2.rename f.ext)
| SType.tforall S E, f => SType.tforall (S.rename f) (E.rename f)
| SType.cforall B E, f => SType.cforall (B.rename f) (E.rename f)
| SType.box T, f => SType.box (T.rename f)
| SType.label S, f => SType.label (S.rename f)

def EType.trename : EType n m k -> FinFun m m' -> EType n m' k
| EType.ex T, f => EType.ex (T.trename f)
| EType.type T, f => EType.type (T.trename f)

def CType.trename : CType n m k -> FinFun m m' -> CType n m' k
| CType.capt C S, f => CType.capt C (S.trename f)

def SType.trename : SType n m k -> FinFun m m' -> SType n m' k
| SType.top, _ => SType.top
| SType.tvar X, f => SType.tvar (f X)
| SType.forall E1 E2, f => SType.forall (E1.trename f) (E2.trename f)
| SType.tforall S E, f => SType.tforall (S.trename f) (E.trename f.ext)
| SType.cforall B E, f => SType.cforall B (E.trename f)
| SType.box T, f => SType.box (T.trename f)
| SType.label S, f => SType.label (S.trename f)

def EType.crename : EType n m k -> FinFun k k' -> EType n m k'
| EType.ex T, f => EType.ex (T.crename f.ext)
| EType.type T, f => EType.type (T.crename f)

def CType.crename : CType n m k -> FinFun k k' -> CType n m k'
| CType.capt C S, f => CType.capt (C.crename f) (S.crename f)

def SType.crename : SType n m k -> FinFun k k' -> SType n m k'
| SType.top, _ => SType.top
| SType.tvar X, _ => SType.tvar X
| SType.forall E1 E2, f => SType.forall (E1.crename f) (E2.crename f)
| SType.tforall S E, f => SType.tforall (S.crename f) (E.crename f)
| SType.cforall B E, f => SType.cforall (B.crename f) (E.crename f.ext)
| SType.box T, f => SType.box (T.crename f)
| SType.label S, f => SType.label (S.crename f)

def EType.weaken (E : EType n m k) : EType (n+1) m k :=
  E.rename FinFun.weaken

def EType.weaken1 (E : EType (n+1) m k) : EType (n+2) m k :=
  E.rename FinFun.weaken.ext

def CType.weaken (C : CType n m k) : CType (n+1) m k :=
  C.rename FinFun.weaken

def SType.weaken (S : SType n m k) : SType (n+1) m k :=
  S.rename FinFun.weaken

def SType.tweaken (S : SType n m k) : SType n (m+1) k :=
  S.trename FinFun.weaken

def EType.cweaken (E : EType n m k) : EType n m (k+1) :=
  E.crename FinFun.weaken

def CType.cweaken (C : CType n m k) : CType n m (k+1) :=
  C.crename FinFun.weaken

def SType.cweaken (S : SType n m k) : SType n m (k+1) :=
  S.crename FinFun.weaken

def SType.cweaken1 (S : SType n m (k+1)) : SType n m (k+2) :=
  S.crename FinFun.weaken.ext

def CType.cweaken1 (T : CType n m (k+1)) : CType n m (k+2) :=
  T.crename FinFun.weaken.ext

def EType.cweaken1 (E : EType n m (k+1)) : EType n m (k+2) :=
  E.crename FinFun.weaken.ext

inductive Cont : Nat -> Nat -> Nat -> Type where
| none : Cont n m k
| cons :
  (t : Term (n+1) m k) ->
  (cont : Cont n m k) ->
  Cont n m k
| conse :
  (t : Term (n+1) m (k+1)) ->
  (cont : Cont n m k) ->
  Cont n m k
| scope :
  (l : Fin n) ->
  Cont n m k ->
  Cont n m k

structure State (n : Nat) (m : Nat) (k : Nat) where
  σ : Store n m k
  cont : Cont n m k
  t : Term n m k

inductive TypedCont : Context n m k -> EType n m k -> Cont n m k -> EType n m k -> CaptureSet n k -> Prop where
| none :
  ESubtyp Γ E E' ->
  TypedCont Γ E Cont.none E' {}
| cons {Ct : CaptureSet n k} :
  Typed (Γ,x: T) t (EType.weaken E) Ct.weaken ->
  WellScoped Γ cont Ct ->
  TypedCont Γ E cont E' C ->
  TypedCont Γ (EType.type T) (Cont.cons t cont) E' (C ∪ Ct)
| conse {Ct : CaptureSet n k} :
  Typed ((Γ.cvar (CBinding.bound CBound.star)).var T) t (EType.weaken (EType.cweaken E)) Ct.cweaken.weaken ->
  WellScoped Γ cont Ct ->
  TypedCont Γ E cont E' C ->
  TypedCont Γ (EType.ex T) (Cont.conse t cont) E' (C ∪ Ct)
| scope :
  Context.LBound Γ x S ->
  TypedCont Γ (S^{}) cont E' C ->
  (Γ ⊢ T0 <: S^{}) ->
  TypedCont Γ (EType.type T0) (Cont.scope x cont) E' C

inductive Store.LBound : Store n m k -> (Fin n) -> SType n m k -> Prop where
| here :
  Store.LBound (Store.label σ S) 0 S.weaken
| there_val :
  Store.LBound σ x S ->
  Store.LBound (Store.val σ t hv) x.succ S.weaken
| there_tval :
  Store.LBound σ x S ->
  Store.LBound (Store.tval σ S') x S.tweaken
| there_cval :
  Store.LBound σ x S ->
  Store.LBound (Store.cval σ C) x S.cweaken
| there_label :
  Store.LBound σ x S ->
  Store.LBound (Store.label σ S') x.succ S.weaken

def Cont.weaken : Cont n m k -> Cont (n+1) m k
| Cont.none => Cont.none
| Cont.cons t cont => Cont.cons t.weaken1 cont.weaken
| Cont.conse t cont => Cont.conse t.weaken1 cont.weaken
| Cont.scope x cont => Cont.scope x.succ cont.weaken

def Cont.cweaken : Cont n m k -> Cont n m (k+1)
| Cont.none => Cont.none
| Cont.cons t cont => Cont.cons t.cweaken cont.cweaken
| Cont.conse t cont => Cont.conse t.cweaken1 cont.cweaken
| Cont.scope x cont => Cont.scope x cont.cweaken

inductive Context.IsTight : Context n m k -> Prop where
| empty : Context.IsTight Context.empty
| var :
  Context.IsTight Γ ->
  Context.IsTight (Γ.var T)
| tvar :
  Context.IsTight Γ ->
  Context.IsTight (Γ.tvar (TBinding.inst S))
| cvar :
  Context.IsTight Γ ->
  Context.IsTight (Γ.cvar (CBinding.inst C))
| label :
  Context.IsTight Γ ->
  Context.IsTight (Γ.label S)

def SSubtyp.dealias_right_cforall.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {B2 E2} (ht : Γ.IsTight) (hd : SType.Dealias Γ S2 (SType.cforall B2 E2)),
    ∃ B1 E1, SType.Dealias Γ S1 (SType.cforall B1 E1)

def SType.open (S : SType (n+1) m k) (x : Fin n) : SType n m k :=
  S.rename (FinFun.open x)

inductive Store : Nat -> Nat -> Nat -> Type where
| empty : Store 0 0 0
| val :
  Store n m k ->
  (t : Term n m k) ->
  t.IsValue ->
  Store (n+1) m k
| tval :
  Store n m k ->
  SType n m k ->
  Store n (m+1) k
| cval :
  Store n m k ->
  CaptureSet n k ->
  Store n m (k+1)
| label :
  Store n m k ->
  SType n m k ->
  Store (n+1) m k

def CaptureSet.copen (C : CaptureSet n (k+1)) (x : Fin k) : CaptureSet n k :=
  C.crename (FinFun.open x)

Fin.succ in Init.Data.Fin.Basic

def SSubtyp.dealias_label_inv.cmotive
  (Γ : Context n m k)
  (C1 : CType n m k)
  (C2 : CType n m k)
  : Prop := True

@[simp]
instance : Union (CaptureSet n k) where
  union := CaptureSet.union

def SSubtyp.dealias_right_forall.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

Coe in Init.Coe

def TVarSubst.narrow
  (hs : SSubtyp Γ S' S) :
  TVarSubst
    (Γ.tvar (TBinding.bound S))
    FinFun.id
    (Γ.tvar (TBinding.bound S')) :=

def SSubtyp.rename_motive1
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop :=
  ∀ {n'} (f : FinFun n n') (Δ : Context n' m k) (ρ : VarMap Γ f Δ),
  ESubtyp Δ (E1.rename f) (E2.rename f)

Or.inl in Init.Prelude

def SSubtyp.dealias_right_tforall.cmotive
  (Γ : Context n m k)
  (C1 : CType n m k)
  (C2 : CType n m k)
  : Prop := True

def Subcapt.tweaken
  (h : Γ ⊢ C1 <:c C2) :
  (Γ.tvar b) ⊢ C1 <:c C2 :=

structure VarMap (Γ : Context n m k) (f : FinFun n n') (Δ : Context n' m k) where
  map : ∀ x E, Γ.Bound x E -> Δ.Bound (f x) (E.rename f)
  tmap : ∀ X b, Γ.TBound X b -> Δ.TBound X (b.rename f)
  cmap : ∀ c b, Γ.CBound c b -> Δ.CBound c (b.rename f)
  lmap : ∀ x S, Γ.LBound x S -> Δ.LBound (f x) (S.rename f)

inductive Cont.HasLabel : Cont n m k -> Fin n -> Cont n m k -> Prop where
| here :
  Cont.HasLabel (Cont.scope l tail) l tail
| there_val :
  Cont.HasLabel cont l tail ->
  Cont.HasLabel (Cont.cons t cont) l tail
| there_tval :
  Cont.HasLabel cont l tail ->
  Cont.HasLabel (Cont.conse t cont) l tail
| there_cval :
  Cont.HasLabel cont l tail ->
  Cont.HasLabel (Cont.scope l' cont) l tail
| there_label :
  Cont.HasLabel cont l tail ->
  Cont.HasLabel (Cont.scope l' cont) l tail

def TVarMap.weaken_cext_ext {Γ : Context n m k} :
  TVarMap
    ((Γ.cvar (CBinding.bound B)).var T)
    FinFun.weaken
    (((Γ.tvar b).cvar (CBinding.bound B)).var T.tweaken) :=

def CaptureSet.open (C : CaptureSet (n+1) k) (x : Fin n) : CaptureSet n k :=
  C.rename (FinFun.open x)

def SSubtyp.dealias_right_label.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

def VarMap.lweaken_cext_ext {Γ : Context n m k} :
  VarMap
    ((Γ.cvar (CBinding.bound b)).var T)
    FinFun.weaken.ext
    (((Γ.label P).cvar (CBinding.bound b.weaken)).var T.weaken) :=

def TVarMap.cext {Γ : Context n m k} {Δ : Context n m' k}
  (ρ : TVarMap Γ f Δ) (b : CBinding n k) :
  TVarMap (Γ.cvar b) f (Δ.cvar b) :=

@[simp]
def CType.tweaken_capt :
  (CType.capt C S).tweaken = CType.capt C S.tweaken :=

def SSubtyp.csubst_motive1
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop :=
  ∀ {k'} (f : FinFun k k') (Δ : Context n m k') (ρ : CVarSubst Γ f Δ),
  ESubtyp Δ (E1.crename f) (E2.crename f)

def TVarSubst.ext {Γ : Context n m k}
  (σ : TVarSubst Γ f Δ)
  (T : CType n m k) :
  TVarSubst (Γ.var T) f (Δ.var (T.trename f)) :=

def CType.topen (C : CType n (m+1) k) (X : Fin m) : CType n m k :=
  C.trename (FinFun.open X)

def EType.topen (E : EType n (m+1) k) (X : Fin m) : EType n m k :=
  E.trename (FinFun.open X)

def Term.copen (t : Term n m (k+1)) (c : Fin k) : Term n m k :=
  t.crename (FinFun.open c)

def SSubtyp.dealias_label_inv.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

def SSubtyp.dealias_forall_inv.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T1 E1 T2 E2}
    (ht : Γ.IsTight)
    (h1 : SType.Dealias Γ S1 (SType.forall T1 E1))
    (h2 : SType.Dealias Γ S2 (SType.forall T2 E2)),
    CSubtyp Γ T2 T1 ∧ ESubtyp (Γ.var T2) E1 E2

inductive Progress : State n m k -> Prop where
| halt_var :
  Progress ⟨σ, Cont.none, Term.var x⟩
| halt_value {t : Term n m k} :
  t.IsValue ->
  Progress ⟨σ, Cont.none, t⟩
| step :
  Reduce state state' ->
  Progress state

def SSubtyp.dealias_right_label.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T2} (ht : Γ.IsTight) (hd : SType.Dealias Γ S2 (SType.label T2)),
    ∃ T1, SType.Dealias Γ S1 (SType.label T1)

def SSubtyp.crename_motive3
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {k'} (f : FinFun k k') (Δ : Context n m k') (ρ : CVarMap Γ f Δ),
  SSubtyp Δ (S1.crename f) (S2.crename f)

def SSubtyp.rename_motive2
  (Γ : Context n m k)
  (C1 : CType n m k)
  (C2 : CType n m k)
  : Prop :=
  ∀ {n'} (f : FinFun n n') (Δ : Context n' m k) (ρ : VarMap Γ f Δ),
  CSubtyp Δ (C1.rename f) (C2.rename f)

def SSubtyp.dealias_right_cforall.cmotive
  (Γ : Context n m k)
  (C1 : CType n m k)
  (C2 : CType n m k)
  : Prop := True

structure TVarSubst (Γ : Context n m k) (f : FinFun m m') (Δ : Context n m' k) where
  map : ∀ x E, Γ.Bound x E -> Δ.Bound x (E.trename f)
  tmap : ∀ X S, Γ.TBound X (TBinding.bound S) ->
    SSubtyp Δ (SType.tvar (f X)) (S.trename f)
  tmap_inst : ∀ X S, Γ.TBound X (TBinding.inst S) ->
    Δ.TBound (f X) (TBinding.inst (S.trename f))
  cmap : ∀ c b, Γ.CBound c b -> Δ.CBound c b
  lmap : ∀ l S, Γ.LBound l S -> Δ.LBound l (S.trename f)

def Store.lookup_inv_bound
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ)
  (hb : Context.Bound Γ x T) :
  ∃ Cv, Typed Γ v (EType.type T) Cv :=

Fin.elim0 in Init.Data.Fin.Basic

def SSubtyp.dealias_right_boxed.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

def SSubtyp.subst_motive3
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {n'} (f : FinFun n n') (Δ : Context n' m k) (ρ : VarSubst Γ f Δ),
  SSubtyp Δ (S1.rename f) (S2.rename f)

inductive SSubtyp : Context n m k -> SType n m k -> SType n m k -> Prop where
| top :
  SSubtyp Γ S SType.top
| refl :
  SSubtyp Γ S S
| trans :
  SSubtyp Γ S1 S2 ->
  SSubtyp Γ S2 S3 ->
  SSubtyp Γ S1 S3
| tvar :
  Context.TBound Γ X (TBinding.bound S) ->
  SSubtyp Γ (SType.tvar X) S
| tinstl :
  Context.TBound Γ X (TBinding.inst S) ->
  SSubtyp Γ S (SType.tvar X)
| tinstr :
  Context.TBound Γ X (TBinding.inst S) ->
  SSubtyp Γ (SType.tvar X) S
| boxed :
  CSubtyp Γ T1 T2 ->
  SSubtyp Γ (□ T1) (□ T2)
| label :
  SSubtyp Γ S2 S1 ->
  SSubtyp Γ (Label[S1]) (Label[S2])
| xforall :
  CSubtyp Γ E2 E1 ->
  ESubtyp (Context.var Γ E2) F1 F2 ->
  SSubtyp Γ (SType.forall E1 F1) (SType.forall E2 F2)
| tforall :
  SSubtyp Γ S2 S1 ->
  ESubtyp (Context.tvar Γ (TBinding.bound S2)) E1 E2 ->
  SSubtyp Γ (SType.tforall S1 E1) (SType.tforall S2 E2)
| cforall :
  Subbound Γ B2 B1 ->
  ESubtyp (Context.cvar Γ (CBinding.bound B2)) E1 E2 ->
  SSubtyp Γ (SType.cforall B1 E1) (SType.cforall B2 E2)

@[simp]
def CBound.weaken_upper :
  (CBound.upper C).weaken = CBound.upper C.weaken :=

def SSubtyp.dealias_boxed_inv.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

@[simp]
instance : EmptyCollection (CaptureSet n k) where
  emptyCollection := CaptureSet.empty

def SSubtyp.rename_motive3
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {n'} (f : FinFun n n') (Δ : Context n' m k) (ρ : VarMap Γ f Δ),
  SSubtyp Δ (S1.rename f) (S2.rename f)

@[simp]
instance : HasSubset (CaptureSet n k) where
  Subset := CaptureSet.Subset

Nat in Init.Prelude

def CVarSubst.ext {Γ : Context n m k}
  (σ : CVarSubst Γ f Δ)
  (T : CType n m k) :
  CVarSubst (Γ.var T) f (Δ.var (T.crename f)) :=

inductive TypedStore : Store n m k -> Context n m k -> Prop where
| empty : TypedStore Store.empty Context.empty
| val :
  TypedStore σ Γ ->
  Typed Γ t (EType.type E) Ct ->
  (hv : t.IsValue) ->
  TypedStore (Store.val σ t hv) (Γ.var E)
| tval :
  TypedStore σ Γ ->
  TypedStore (Store.tval σ S) (Γ.tvar (TBinding.inst S))
| cval :
  TypedStore σ Γ ->
  TypedStore (Store.cval σ C) (Γ.cvar (CBinding.inst C))
| label :
  TypedStore σ Γ ->
  TypedStore (Store.label σ S) (Γ.label S)

def CVarMap.weaken {Γ : Context n m k} :
  CVarMap Γ FinFun.weaken (Γ.cvar b) :=

def SSubtyp.tsubst_motive2
  (Γ : Context n m k)
  (C1 : CType n m k)
  (C2 : CType n m k)
  : Prop :=
  ∀ {m'} (f : FinFun m m') (Δ : Context n m' k) (ρ : TVarSubst Γ f Δ),
  CSubtyp Δ (C1.trename f) (C2.trename f)

def Typed.tweaken
  (h : Typed Γ t E Ct) :
  Typed (Γ.tvar b) t.tweaken E.tweaken Ct :=

@[simp]
def EType.cweaken_type :
  (EType.type T).cweaken = EType.type (T.cweaken) :=

HasSubset in Init.Core

abs in Mathlib.Algebra.Order.Group.Unbundled.Abs

inductive WellScoped : Context n m k -> Cont n m k -> CaptureSet n k -> Prop where
| empty :
  WellScoped Γ cont {}
| union :
  WellScoped Γ cont C1 ->
  WellScoped Γ cont C2 ->
  WellScoped Γ cont (C1 ∪ C2)
| singleton :
  Context.Bound Γ x (S^C) ->
  WellScoped Γ cont C ->
  WellScoped Γ cont {x=x}
| csingleton :
  Context.CBound Γ c (CBinding.inst C) ->
  WellScoped Γ cont C ->
  WellScoped Γ cont {c=c}
| cbound :
  Context.CBound Γ c (CBinding.bound (CBound.upper C)) ->
  WellScoped Γ cont C ->
  WellScoped Γ cont {c=c}
| label :
  Context.LBound Γ x S ->
  Cont.HasLabel cont x tail ->
  WellScoped Γ cont {x=x}

def VarMap.ext {Γ : Context n m k} {Δ : Context n' m k}
  (ρ : VarMap Γ f Δ) (E : CType n m k) :
  VarMap (Γ.var E) f.ext (Δ.var (E.rename f)) :=

@[simp]
def EType.tweaken_type :
  (EType.type T).tweaken = EType.type (T.tweaken) :=

def TVarMap.weaken {Γ : Context n m k} :
  TVarMap Γ FinFun.weaken (Γ.tvar b) :=

def CVarSubst.instantiate {Γ : Context n m k} :
  CVarSubst
    (Γ.cvar (CBinding.bound CBound.star))
    FinFun.id
    (Γ.cvar (CBinding.inst C)) :=

def CType.open (C : CType (n+1) m k) (x : Fin n) : CType n m k :=
  C.rename (FinFun.open x)

def Term.open (t : Term (n+1) m k) (x : Fin n) : Term n m k :=
  t.rename (FinFun.open x)

inductive CSubtyp : Context n m k -> CType n m k -> CType n m k -> Prop where
| capt :
  (Γ ⊢ C1 <:c C2) ->
  SSubtyp Γ S1 S2 ->
  CSubtyp Γ (CType.capt C1 S1) (CType.capt C2 S2)

def VarMap.cext {Γ : Context n m k} {Δ : Context n' m k}
  (ρ : VarMap Γ f Δ) (b : CBinding n k) :
  VarMap (Γ.cvar b) f (Δ.cvar (b.rename f)) :=

Exists in Init.Core

def TVarSubst.text {Γ : Context n m k}
  (σ : TVarSubst Γ f Δ)
  (T : TBinding n m k) :
  TVarSubst (Γ.tvar T) f.ext (Δ.tvar (T.trename f)) :=

EmptyCollection in Init.Core

Or in Init.Prelude

Union in Init.Core
</all_available_defs>

<all_available_lemmas>
theorem CaptureSet.ext_rename_singleton_zero {f : FinFun n n'} :
  ({x=0} : CaptureSet (n+1) k).rename f.ext = {x=0}

theorem Typed.forall_inv {v : Term n m k}
  (hg : Γ.IsTight)
  (hv : v.IsValue)
  (ht : Typed Γ v (EType.type (CType.capt Cv (SType.forall T E))) Ct) :
  ∃ T0 t, v = Term.lam T0 t

theorem CaptureSet.copen_cweaken_ext {C : CaptureSet n (k+1)} :
  (C.crename (FinFun.weaken.ext)).crename (FinFun.open 0) = C

theorem TBinding.rename_id {b : TBinding n m k} :
  b.rename FinFun.id = b

theorem EType.cweaken1_weaken (E : EType n m (k+1)) :
  E.weaken.cweaken1 = E.cweaken1.weaken

theorem Typed.cnarrow
  (h : Typed (Γ,c<:B) t E Ct)
  (hs : Subbound Γ B' B) :
  Typed (Γ,c<:B') t E Ct

theorem Typed.var_inv_capt
  (hx : Typed Γ (Term.var x) E Cx) :
  Γ ⊢ ({x=x}) <:c Cx

theorem SType.dealias_forall_inj'
  (he1 : S1 = SType.forall T1 E1) (he2 : S2 = SType.forall T2 E2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  T1 = T2 ∧ E1 = E2

theorem SType.tweaken_crename {S : SType n m k} :
  (S.crename f).tweaken = S.tweaken.crename f

theorem CSubtyp.crename
  (h : CSubtyp Γ C1 C2)
  (ρ : CVarMap Γ f Δ) :
  CSubtyp Δ (C1.crename f) (C2.crename f)

theorem EType.crename_open {E : EType (n+1) m k} :
  (E.open x).crename f = (E.crename f).open x

theorem CType.weaken_rename {C : CType n m k} :
  (C.rename f).weaken = C.weaken.rename f.ext

theorem Store.label_lookup_exists {σ : Store n m k} {x : Fin n}
  (hs : TypedStore σ Γ)
  (hx : Typed Γ (Term.var x) (EType.type (Label[S]^C)) Cx) :
  ∃ S0, Store.LBound σ x S0

theorem Typed.canonical_form_pack
  (ht : Γ.IsTight)
  (h : Typed Γ (Term.pack C x) (EType.ex T) Ct) :
  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x}

theorem TBinding.cweaken_crename {b : TBinding n m k} :
  (b.crename f).cweaken = b.cweaken.crename f.ext

theorem WellScoped.var_inv
  (hsc : WellScoped Γ cont {x=x})
  (hbx : Γ.Bound x (S^C)) :
  WellScoped Γ cont C

theorem CBound.crename_rename_comm {b : CBound n k} :
  (b.crename f).rename g = (b.rename g).crename f

theorem CaptureSet.rename_rename {C : CaptureSet n k} :
  (C.rename f).rename g = C.rename (g ∘ f)

theorem WellScoped.scope
  (hsc : WellScoped Γ cont C) :
  WellScoped Γ (Cont.scope x cont) C

theorem CSubtyp.weaken
  (h : CSubtyp Γ E1 E2) :
  CSubtyp (Γ.var T) E1.weaken E2.weaken

theorem SType.crename_copen {S : SType n m (k+1)} :
  (S.copen c).crename f = (S.crename f.ext).copen (f c)

theorem TypedStore.is_tight
  (h : TypedStore σ Γ) :
  Γ.IsTight

@[simp]
lemma TBinding.weaken_bound: (TBinding.bound T).weaken = TBinding.bound (T.weaken)

theorem IsValue.trename_l' {t : Term n m k} {t0 : Term n m' k}
  (he : t0 = t.trename f)
  (hv : t0.IsValue) :
  t.IsValue

theorem SType.tvar_tweaken_succ :
  (SType.tvar X : SType n m k).tweaken = SType.tvar X.succ

theorem SType.dealias_boxed_inj'
  (he1 : S1 = SType.box T1) (he2 : S2 = SType.box T2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  T1 = T2

theorem CaptureSet.crename_crename {C : CaptureSet n k} :
  (C.crename f).crename g = C.crename (g ∘ f)

theorem IsValue.crename_l {t : Term n m k}
  (hv : (t.crename f).IsValue) :
  t.IsValue

theorem Store.value_typing_label_absurd
  (hg : Γ.IsTight)
  (ht : Typed Γ v (EType.type (Label[S]^C)) Cv)
  (hv : v.IsValue) : False

theorem EType.tweaken_weaken (E : EType n m k) :
  E.weaken.tweaken = E.tweaken.weaken

theorem FinFun.comp_weaken {f : FinFun n n'} :
  weaken ∘ f = f.ext ∘ weaken

theorem ESubtyp.trans
  (h1 : ESubtyp Γ E1 E2)
  (h2 : ESubtyp Γ E2 E3) :
  ESubtyp Γ E1 E3

theorem CType.crename_id {T : CType n m k} :
  T.crename FinFun.id = T

theorem Typed.invoke_inv' {Γ : Context n m k}
  (he : t0 = Term.invoke x y)
  (ht : Typed Γ t0 E Ct) :
  ∃ S0 C0,
    Typed Γ (Term.var x) (Label[S0]^C0) {x=x} ∧
    Typed Γ (Term.var y) (EType.type (S0^{})) {x=y}

theorem ESubtyp.sub_type_inv
  (h : ESubtyp Γ E1 (EType.type T2)) :
  ∃ T1, E1 = EType.type T1 ∧ CSubtyp Γ T1 T2

theorem EType.cweaken_eq_inv {E : EType n m k}
  (heq : EType.type (CType.capt C S) = E.cweaken) :
  ∃ C0 S0, E = EType.type (CType.capt C0 S0) ∧ C0.cweaken = C ∧ S0.cweaken = S

theorem CType.trename_rename_comm (T : CType n m k) (f : FinFun n n') (g : FinFun m m') :
  (T.trename g).rename f = (T.rename f).trename g

theorem Typed.tapp_inv'
  (he : t0 = Term.tapp x X)
  (h : Typed Γ t0 E Ct) :
  ∃ Cf F E0,
    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {x=x}
    ∧ E0 = F.topen X
    ∧ ESubtyp Γ E0 E

theorem Term.copen_cweaken_ext {t : Term n m (k+1)} :
  (t.crename (FinFun.weaken.ext)).crename (FinFun.open 0) = t

theorem CaptureSet.cweaken_rename_comm {C : CaptureSet n k} {f : FinFun n n'} :
  (C.cweaken).rename f = (C.rename f).cweaken

theorem SType.dealias_label_inj'
  (he1 : S1 = SType.label T1) (he2 : S2 = SType.label T2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  T1 = T2

theorem CaptureSet.rename_empty :
  ({} : CaptureSet n k).rename f = {}

theorem SType.weaken_rename {S : SType n m k} :
  (S.rename f).weaken = S.weaken.rename f.ext

theorem Typed.cforall_inv {v : Term n m k}
  (hg : Γ.IsTight)
  (hv : v.IsValue)
  (ht : Typed Γ v (EType.type (CType.capt Cv (SType.cforall B E))) Ct) :
  ∃ B0 t, v = Term.clam B0 t

theorem CType.tweaken_crename {C : CType n m k} :
  (C.crename f).tweaken = C.tweaken.crename f

theorem Term.trename_trename {t : Term n m k} {f : FinFun m m'} {g : FinFun m' m''} :
  (t.trename f).trename g = t.trename (g.comp f)

theorem CBinding.cweaken_rename_comm {b : CBinding n k} :
  b.cweaken.rename f = (b.rename f).cweaken

theorem Store.lookup_inv_typing_alt
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ)
  (hx : Typed Γ (Term.var x) (EType.type (S^C)) Cx) :
  ∃ C0 Cv0, Typed Γ v (EType.type (S^C0)) Cv0

theorem EType.trename_rename_comm (E : EType n m k) (f : FinFun n n') (g : FinFun m m') :
  (E.trename g).rename f = (E.rename f).trename g

theorem Typed.letex_inv {Γ : Context n m k}
  (h : Typed Γ (Term.letex t u) E Ct) :
  ∃ T E0,
    Typed Γ t (EType.ex T) Ct ∧
    Typed ((Γ,c<:*).var T) u E0.cweaken.weaken Ct.cweaken.weaken ∧
    ESubtyp Γ E0 E

theorem WellScoped.tweaken
  (h : WellScoped Γ cont Ct) :
  WellScoped (Γ.tvar b) cont.tweaken Ct

theorem Term.rename_id {t : Term n m k} :
  t.rename FinFun.id = t

theorem Subcapt.refl :
  Subcapt Γ C C

theorem Store.lookup_inv_typing
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ)
  (hx : Typed Γ (Term.var x) (EType.type (S^C)) Cx) :
  ∃ S0 C0 Cv0,
    Typed Γ v (EType.type (S0^C0)) Cv0 ∧
    Γ.Bound x (S0^C0) ∧
    (Γ ⊢ (S0^{x=x}) <: (S^C))

theorem EType.tweaken_ex (T : CType n m (k+1)) :
  (EType.ex T).tweaken = EType.ex T.tweaken

theorem SSubtyp.crename
  (h : SSubtyp Γ S1 S2)
  (ρ : CVarMap Γ f Δ) :
  SSubtyp Δ (S1.crename f) (S2.crename f)

theorem SType.rename_id {S : SType n m k} :
  S.rename FinFun.id = S

theorem SSubtyp.sub_dealias_cforall_inv
  (ht : Γ.IsTight)
  (h1 : SType.Dealias Γ S1 (SType.cforall B1 E1))
  (h2 : SType.Dealias Γ S2 (SType.cforall B2 E2))
  (hs : SSubtyp Γ S1 S2) :
  Subbound Γ B2 B1 ∧ ESubtyp (Γ.cvar (CBinding.bound B2)) E1 E2

theorem Typed.val_precise_cv
  (ht : Typed Γ t (EType.type T) Ct)
  (hv : t.IsValue) :
  Typed Γ t (EType.type T) {}

theorem Subcapt.crename
  (h : Subcapt Γ C1 C2)
  (ρ : CVarMap Γ f Δ) :
  Subcapt Δ (C1.crename f) (C2.crename f)

theorem Subbound.subst
  (h : Subbound Γ B1 B2)
  (σ : VarSubst Γ f Δ) :
  Subbound Δ (B1.rename f) (B2.rename f)

theorem ESubtyp.weaken
  (h : ESubtyp Γ E1 E2) :
  ESubtyp (Γ.var T) E1.weaken E2.weaken

theorem Typed.canonical_form_pack'
  (ht : Γ.IsTight)
  (he1 : t0 = Term.pack C x)
  (he2 : E0 = EType.ex T)
  (h : Typed Γ t0 E0 Ct) :
  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x}

theorem CSubtyp.trename
  (h : CSubtyp Γ T1 T2)
  (ρ : TVarMap Γ f Δ) :
  CSubtyp Δ (T1.trename f) (T2.trename f)

theorem TBinding.rename_rename {b : TBinding n m k} :
  (b.rename f).rename g = b.rename (g ∘ f)

theorem EType.tweaken_trename {E : EType n m k} :
  (E.trename f).tweaken = E.tweaken.trename f.ext

theorem ESubtyp.sub_type_inv'
  (he : E2 = EType.type T2)
  (h : ESubtyp Γ E1 E2) :
  ∃ T1, E1 = EType.type T1 ∧ CSubtyp Γ T1 T2

theorem SType.dealias_tforall_inj'
  (he1 : S1 = SType.tforall T1 E1) (he2 : S2 = SType.tforall T2 E2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  T1 = T2 ∧ E1 = E2

theorem Subbound.tsubst
  (h : Subbound Γ B1 B2)
  (σ : TVarSubst Γ f Δ) :
  Subbound Δ B1 B2

theorem SType.weaken_crename {S : SType n m k} :
  (S.crename f).weaken = S.weaken.crename f

theorem CBinding.rename_id {b : CBinding n k} :
  b.rename FinFun.id = b

theorem CType.rename_capt :
  (CType.capt C S).rename f = CType.capt (C.rename f) (S.rename f)

theorem Typed.tforall_inv {v : Term n m k}
  (hg : Γ.IsTight)
  (hv : v.IsValue)
  (ht : Typed Γ v (EType.type (CType.capt Cv (SType.tforall X E))) Ct) :
  ∃ X t, v = Term.tlam X t

theorem CType.tweaken_rename {C : CType n m k} :
  C.tweaken.rename f = (C.rename f).tweaken

theorem Typed.weaken
  (h : Typed Γ t E Ct) :
  Typed (Γ.var T) t.weaken E.weaken Ct.weaken

theorem Store.bound_type
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ) :
  ∃ T0, Context.Bound Γ x T0

theorem TypedCont.weaken
  (h : TypedCont Γ E t E' C0) :
  TypedCont (Γ.var T) E.weaken t.weaken E'.weaken C0.weaken

theorem CaptureSet.open_weaken_ext {C : CaptureSet (n+1) k} :
  (C.rename (FinFun.weaken.ext)).rename (FinFun.open 0) = C

theorem Typed.canonical_form_lam'
  (ht : Γ.IsTight)
  (he1 : t0 = Term.lam T t) (hd2 : SType.Dealias Γ S0 (SType.forall T' E))
  (he2 : E0 = EType.type (CType.capt Cf S0))
  (h : Typed Γ t0 E0 Ct0) :
  CSubtyp Γ T' T ∧
  Typed (Γ.var T') t E (Cf.weaken ∪ {x=0})

theorem CaptureSet.crename_singleton {x : Fin n} {f : FinFun k k'} :
  {x=x}.crename f = {x=x}

theorem EType.cweaken_crename {E : EType n m k} :
  (E.crename f).cweaken = E.cweaken.crename f.ext

theorem EType.trename_id {E : EType n m k} :
  E.trename FinFun.id = E

theorem ESubtyp.cnarrow
  (h : ESubtyp (Γ,c<:B) E1 E2)
  (hs : Subbound Γ B' B) :
  ESubtyp (Γ,c<:B') E1 E2

theorem TBinding.crename_crename {b : TBinding n m k} :
  (b.crename f).crename g = b.crename (g ∘ f)

theorem Typed.tapp_inv
  (h : Typed Γ (Term.tapp x X) E Ct) :
  ∃ Cf F E0,
    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {x=x}
    ∧ E0 = F.topen X
    ∧ ESubtyp Γ E0 E

theorem ESubtyp.narrow
  (h : ESubtyp (Γ.var T) E1 E2)
  (hs : CSubtyp Γ T' T) :
  ESubtyp (Γ.var T') E1 E2

theorem EType.cweaken_ex (T : CType n m (k+1)) :
  (EType.ex T).cweaken = EType.ex T.cweaken1

theorem TBinding.crename_rename_comm {b : TBinding n m k} :
  (b.crename f).rename g = (b.rename g).crename f

theorem Typed.weaken_cext_ext {Γ : Context n m k}
  (h : Typed ((Γ.cvar (CBinding.bound B)).var T) t E Ct) :
  Typed (((Γ.var P).cvar (CBinding.bound B.weaken)).var T.weaken) t.weaken1 E.weaken1 Ct.weaken1

theorem IsValue.rename_r {t : Term n m k}
  (hv : t.IsValue) :
  (t.rename f).IsValue

theorem CaptureSet.crename_csingleton {x : Fin k} {f : FinFun k k'} :
  ({c=x} : CaptureSet n k).crename f = {c=f x}

theorem Subcapt.csubst
  (h : Subcapt Γ C1 C2)
  (σ : CVarSubst Γ f Δ) :
  Subcapt Δ (C1.crename f) (C2.crename f)

theorem TBinding.trename_trename {b : TBinding n m k} :
  (b.trename f).trename g = b.trename (g ∘ f)

theorem Subcapt.subst
  (h : Subcapt Γ C1 C2)
  (σ : VarSubst Γ f Δ) :
  Subcapt Δ (C1.rename f) (C2.rename f)

theorem Typed.crename
  {Γ : Context n m k} {Δ : Context n m k'}
  (h : Typed Γ t E Ct)
  (ρ : CVarMap Γ f Δ) :
  Typed Δ (t.crename f) (E.crename f) (Ct.crename f)

theorem EType.trename_topen {E : EType n (m+1) k} :
  (E.topen X).trename f = (E.trename f.ext).topen (f X)

theorem CBinding.cweaken_bound :
  (CBinding.bound b : CBinding n k).cweaken = (CBinding.bound b.cweaken)

theorem CType.cweaken_copen_id {T : CType n m k} :
  T.cweaken.crename (FinFun.open x) = T

theorem Subbound.trans
  (h1 : Subbound Γ B1 B2)
  (h2 : Subbound Γ B2 B3) :
  Subbound Γ B1 B3

theorem IsValue.crename_l' {t : Term n m k} {t0 : Term n m k'}
  (he : t0 = t.crename f)
  (hv : t0.IsValue) :
  t.IsValue

theorem TBinding.tweaken_crename {b : TBinding n m k} :
  (b.crename f).tweaken = b.tweaken.crename f

theorem Typed.trename
  {Γ : Context n m k} {Δ : Context n m' k}
  (h : Typed Γ t E Ct)
  (ρ : TVarMap Γ f Δ) :
  Typed Δ (t.trename f) (E.trename f) Ct

theorem EType.trename_trename (E : EType n m k) (f : FinFun m m') (g : FinFun m' m'') :
  (E.trename f).trename g = E.trename (g ∘ f)

theorem Typed.capp_inv_capt'
  (he : t0 = Term.capp x c)
  (ht : Typed Γ t0 E Ct) :
  Γ ⊢ ({x=x}) <:c Ct

theorem ESubtyp.tsubst
  (h : ESubtyp Γ E1 E2)
  (σ : TVarSubst Γ f Δ) :
  ESubtyp Δ (E1.trename f) (E2.trename f)

theorem ESubtyp.tweaken
  (h : ESubtyp Γ E1 E2) :
  ESubtyp (Γ.tvar b) E1.tweaken E2.tweaken

theorem Typed.var_inv
  (h : Typed Γ (Term.var x) (EType.type T) Ct) (hb : Γ.Bound x T0) :
  ∃ C0 S0, Γ.Bound x (CType.capt C0 S0) ∧ CSubtyp Γ (CType.capt {x=x} S0) T

theorem EType.tweaken_rename {E : EType n m k} :
  E.tweaken.rename f = (E.rename f).tweaken

theorem SSubtyp.csubst
  (h : SSubtyp Γ S1 S2)
  (σ : CVarSubst Γ f Δ) :
  SSubtyp Δ (S1.crename f) (S2.crename f)

@[simp]
lemma CBinding.weaken_inst: (CBinding.inst T).weaken = CBinding.inst (T.weaken)

theorem Typed.bindt_inv' {Γ : Context n m k}
  (he : t0 = Term.bindt T t)
  (h : Typed Γ t0 E Ct0) :
  ∃ E0,
    Typed (Γ.tvar (TBinding.inst T)) t E0.tweaken Ct0 ∧
    ESubtyp Γ E0 E

theorem EType.crename_topen {E : EType n (m+1) k} :
  (E.topen X).crename f = (E.crename f).topen X

theorem Typed.cinstantiate_extvar {Γ : Context n m k}
  (h : Typed ((Γ,c<:CBound.star).var P) t E Ct) :
  Typed ((Γ,c:=C).var P) t E Ct

theorem TBinding.cweaken_rename_comm {b : TBinding n m k} :
  b.cweaken.rename f = (b.rename f).cweaken

theorem SSubtyp.sub_dealias_tforall_inv
  (ht : Γ.IsTight)
  (h1 : SType.Dealias Γ S1 (SType.tforall T1 E1))
  (h2 : SType.Dealias Γ S2 (SType.tforall T2 E2))
  (hs : SSubtyp Γ S1 S2) :
  SSubtyp Γ T2 T1 ∧ ESubtyp (Γ.tvar (TBinding.bound T2)) E1 E2

theorem EType.rename_id {E : EType n m k} :
  E.rename FinFun.id = E

theorem CaptureSet.Subset.crename {C1 C2 : CaptureSet n k}
  (h : C1 ⊆ C2) :
  C1.crename f ⊆ C2.crename f

theorem CBound.crename_id {b : CBound n k} :
  b.crename FinFun.id = b

theorem EType.rename_topen :
  (EType.topen E X).rename f = (E.rename f).topen X

theorem Cont.has_label_tail_inv
  (htc : TypedCont Γ E1 cont E2 Ct)
  (hb : Γ.LBound x S0)
  (hh : cont.HasLabel x tail) :
  ∃ Ct1, TypedCont Γ (S0^{}) tail E2 Ct1

theorem SSubtyp.subst
  (h : SSubtyp Γ S1 S2)
  (σ : VarSubst Γ f Δ) :
  SSubtyp Δ (S1.rename f) (S2.rename f)

theorem WellScoped.conse
  (hsc : WellScoped Γ cont C) :
  WellScoped Γ (Cont.conse u cont) C

theorem TBinding.weaken_rename {b : TBinding n m k} :
  (b.rename f).weaken = b.weaken.rename f.ext

theorem CType.cweaken_trename {E : CType n m k} :
  (E.trename f).cweaken = E.cweaken.trename f

theorem TBinding.crename_id {b : TBinding n m k} :
  b.crename FinFun.id = b

theorem SType.dealias_forall_inj
  (h1 : SType.Dealias Γ S (SType.forall T1 E1))
  (h2 : SType.Dealias Γ S (SType.forall T2 E2)) :
  T1 = T2 ∧ E1 = E2

theorem CaptureSet.cweaken_union {C1 C2 : CaptureSet n k} :
  (C1 ∪ C2).cweaken = C1.cweaken ∪ C2.cweaken

theorem IsValue.rename_l' {t : Term n m k} {t0 : Term n' m k}
  (he : t0 = t.rename f)
  (hv : t0.IsValue) :
  t.IsValue

theorem CaptureSet.cweaken_monotone {C1 C2 : CaptureSet n k}
  (h : C1 ⊆ C2) :
  C1.cweaken ⊆ C2.cweaken

theorem SSubtyp.sub_dealias_forall_inv
  (ht : Γ.IsTight)
  (h1 : SType.Dealias Γ S1 (SType.forall T1 E1))
  (h2 : SType.Dealias Γ S2 (SType.forall T2 E2))
  (hs : SSubtyp Γ S1 S2) :
  CSubtyp Γ T2 T1 ∧ ESubtyp (Γ.var T2) E1 E2

theorem Subbound.csubst
  (h : Subbound Γ B1 B2)
  (σ : CVarSubst Γ f Δ) :
  Subbound Δ (B1.crename f) (B2.crename f)

theorem IsValue.trename_l {t : Term n m k}
  (hv : (t.trename f).IsValue) :
  t.IsValue

theorem Typing.inv_subcapt
  (h : Typed Γ (Term.var x) (EType.type (CType.capt C S)) C0) :
  Subcapt Γ {x=x} C

theorem Typed.bound_typing
  (hb : Context.Bound Γ x T) :
  Typed Γ (Term.var x) (EType.type T) {x=x}

theorem EType.trename_copen {E : EType n m (k+1)} :
  (E.copen c).trename f = (E.trename f).copen c

theorem FinFun.open_comp_weaken :
  (FinFun.open x) ∘ weaken = id

theorem FinFun.ext_comp_ext {f : FinFun n n'} {g : FinFun n' n''} :
  g.ext ∘ f.ext = FinFun.ext (g ∘ f)

theorem SType.dealias_label_inj
  (h1 : SType.Dealias Γ S (SType.label T1))
  (h2 : SType.Dealias Γ S (SType.label T2)) :
  T1 = T2

theorem CaptureSet.crename_rename_comm {C : CaptureSet n k} {f : FinFun n n'} {g : FinFun k k'} :
  (C.rename f).crename g = (C.crename g).rename f

theorem SType.weaken_trename {S : SType n m k} :
  (S.trename f).weaken = S.weaken.trename f

theorem EType.tweaken_cweaken (E : EType n m k) :
  E.cweaken.tweaken = E.tweaken.cweaken

theorem Typed.lweaken
  (h : Typed Γ t E Ct) :
  Typed (Γ.label S) t.weaken E.weaken Ct.weaken

theorem CBinding.eq_inst_cweaken_inv {b : CBinding n k}
  (h : CBinding.inst C = b.cweaken) :
  ∃ C0, b = CBinding.inst C0

theorem Subbound.refl {B : CBound n k} :
  Subbound Γ B B

theorem Typed.var_inv_capt'
  (he : t0 = Term.var x)
  (hx : Typed Γ t0 E Cx) :
  Γ ⊢ ({x=x}) <:c Cx

theorem EType.weaken_cweaken (E : EType n m k) :
  E.cweaken.weaken = E.weaken.cweaken

theorem preservation
  (hr : Reduce state state')
  (ht : TypedState state Γ E) :
  Preserve Γ E state'

theorem Subbound.crename
  (h : Subbound Γ B1 B2)
  (ρ : CVarMap Γ f Δ) :
  Subbound Δ (B1.crename f) (B2.crename f)

theorem Typed.canonical_form_clam
  (ht : Γ.IsTight)
  (h : Typed Γ (Term.clam B t) (EType.type ((∀[c<:B']E)^Cf)) Ct) :
  Subbound Γ B' B ∧
    Typed (Γ,c<:B') t E Cf.cweaken

theorem CaptureSet.cweaken1_cweaken (C : CaptureSet n k) :
  C.cweaken.cweaken1 = C.cweaken.cweaken

theorem Typed.app_inv
  (h : Typed Γ (Term.app x y) E Ct) :
  ∃ T Cf F E0, Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.forall T F))) {x=x}
    ∧ Typed Γ (Term.var y) (EType.type T) {x=y}
    ∧ E0 = F.open y
    ∧ ESubtyp Γ E0 E

theorem CType.copen_rename_comm {C : CType n m (k+1)} :
  (C.copen x).rename f = (C.rename f).copen x

theorem EType.open_weaken_ext {E : EType (n+1) m k} :
  (E.rename (FinFun.weaken.ext)).rename (FinFun.open 0) = E

theorem CBinding.crename_crename {b : CBinding n k} :
  (b.crename f).crename g = b.crename (g ∘ f)

theorem Typed.capp_inv_capt
  (ht : Typed Γ (Term.capp x c) E Ct) :
  Γ ⊢ ({x=x}) <:c Ct

theorem IsValue.crename_r {t : Term n m k}
  (hv : t.IsValue) :
  (t.crename f).IsValue

theorem CSubtyp.cweaken
  (h : CSubtyp Γ E1 E2) :
  CSubtyp (Γ.cvar b) E1.cweaken E2.cweaken

theorem TBinding.tweaken_trename {b : TBinding n m k} :
  (b.trename f).tweaken = b.tweaken.trename f.ext

theorem SSubtyp.tsubst
  (h : SSubtyp Γ S1 S2)
  (σ : TVarSubst Γ f Δ) :
  SSubtyp Δ (S1.trename f) (S2.trename f)

theorem CBinding.rename_rename {b : CBinding n k} :
  (b.rename f).rename g = b.rename (g ∘ f)

theorem EType.cweaken1_cweaken (E : EType n m k) :
  E.cweaken.cweaken1 = E.cweaken.cweaken

theorem Typing.inv_subcapt'
  (he1 : t0 = Term.var x) (he2 : E0 = EType.type (CType.capt C S))
  (h : Typed Γ t0 E0 C0) :
  Subcapt Γ {x=x} C

theorem Term.IsValue.tweaken
  (hv : Term.IsValue t) :
  Term.IsValue t.tweaken

theorem Typed.tsubst
  {Γ : Context n m k} {Δ : Context n m' k}
  (h : Typed Γ t E Ct)
  (σ : TVarSubst Γ f Δ) :
  Typed Δ (t.trename f) (E.trename f) Ct

theorem SType.dealias_tforall_inj
  (h1 : SType.Dealias Γ S (SType.tforall T1 E1))
  (h2 : SType.Dealias Γ S (SType.tforall T2 E2)) :
  T1 = T2 ∧ E1 = E2

theorem TypedCont.tweaken
  (h : TypedCont Γ E t E' C0) :
  TypedCont (Γ.tvar S) E.tweaken t.tweaken E'.tweaken C0
</all_available_lemmas>

<local_ctx>
import Capless.Context

import Capless.Store

namespace Capless
</local_ctx>

<target_theorem>
theorem Context.tight_bound_tvar_absurd
  (ht : Context.IsTight Γ)
  (hb : Context.TBound Γ X (TBinding.bound S)) : False :=
</target_theorem>

