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

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.tweaken (t : Term n m k) : Term n (m+1) k := t.trename FinFun.weaken

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

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)

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) :=

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

def Typed.cweaken
  (h : Typed Γ t E Ct) :
  Typed (Γ.cvar b) t.cweaken E.cweaken Ct.cweaken :=

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.Bound : Context n m k -> Fin n -> CType n m k -> Prop where
| here : Bound (var Γ0 E) 0 E.weaken
| there_var :
  Bound Γ x E ->
  Bound (var Γ E') (Fin.succ x) E.weaken
| there_tvar :
  Bound Γ x E ->
  Bound (tvar Γ b) x E.tweaken
| there_cvar :
  Bound Γ x E ->
  Bound (cvar Γ b) x E.cweaken
| there_label :
  Bound Γ x E ->
  Bound (label Γ S) (Fin.succ x) E.weaken

inductive Context.CBound : Context n m k -> Fin k -> CBinding n k -> Prop where
| here : CBound (cvar Γ0 b) 0 b.cweaken
| there_var :
  CBound Γ x b ->
  CBound (var Γ E) x b.weaken
| there_tvar :
  CBound Γ x b ->
  CBound (tvar Γ b') x b
| there_cvar :
  CBound Γ x b ->
  CBound (cvar Γ b') (Fin.succ x) b.cweaken
| there_label :
  CBound Γ x b ->
  CBound (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 Typed : Context n m k -> Term n m k -> EType n m k -> CaptureSet n k -> Prop where
| var :
  Context.Bound Γ x (S^C) ->
  Typed Γ (Term.var x) (S^{x=x}) {x=x}
| label :
  Context.LBound Γ x S ->
  Typed Γ (Term.var x) (Label[S]^{x=x}) {x=x}
| pack :
  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x} ->
  Typed Γ (Term.pack C x) (∃c.T) {}
| sub :
  Typed Γ t E1 C1 ->
  (Γ ⊢ C1 <:c C2) ->
  (Γ ⊢ E1 <:e E2) ->
  Typed Γ t E2 C2
| abs {C : CaptureSet n k} :
  Typed (Γ,x:T) t E (C.weaken ∪ {x=0}) ->
  Typed Γ (λ(x:T)t) ((∀(x:T)E)^C) {}
| tabs {C : CaptureSet n k} :
  Typed (Γ,X<:S) t E C ->
  Typed Γ (λ[X<:S]t) ((∀[X<:S]E)^C) {}
| cabs {C : CaptureSet n k} :
  Typed (Γ,c<:B) t E C.cweaken ->
  Typed Γ (λ[c<:B]t) ((∀[c<:B]E)^C) {}
| app :
  Typed Γ (Term.var x) (EType.type (∀(x:T)E)^C) {x=x} ->
  Typed Γ (Term.var y) T {x=y} ->
  Typed Γ (Term.app x y) (E.open y) ({x=x} ∪ {x=y})
| invoke :
  Typed Γ (Term.var x) (EType.type (Label[S])^C) {x=x} ->
  Typed Γ (Term.var y) (S^{}) {x=y} ->
  Typed Γ (Term.invoke x y) E ({x=x} ∪ {x=y})
| tapp :
  Typed Γ (Term.var x) (EType.type (∀[X<:SType.tvar X]E)^C) {x=x} ->
  Typed Γ (Term.tapp x X) (E.topen X) {x=x}
| capp :
  Typed Γ (Term.var x) (EType.type (∀[c<:CBound.upper {c=c}]E)^C) {x=x} ->
  Typed Γ (Term.capp x c) (E.copen c) {x=x}
| letin :
  Typed Γ t (EType.type T) C ->
  Typed (Γ,x: T) u E.weaken C.weaken ->  
  Typed Γ (let x=t in u) E C
| letex :
  Typed Γ t (EType.ex T) C ->
  Typed ((Γ,c<:*),x: T) u E.cweaken.weaken C.cweaken.weaken ->
  Typed Γ (let (c,x)=t in u) E C
| bindt :
  Typed (Γ,X:=S) t E.tweaken C ->
  Typed Γ (let X=S in t) E C
| bindc :
  Typed (Γ,c:=C) t E.cweaken C0.cweaken ->
  Typed Γ (let c=C in t) E C0
| boundary {Γ : Context n m k} {S : SType n m k} :
  Typed
    ((Γ,c<:CBound.star),x: Label[S.cweaken]^{c=0})
    t
    (S.cweaken.weaken^{}) (C.cweaken.weaken ∪ {c=0} ∪ {x=0}) ->
  Typed Γ (boundary: S in t) (S^CaptureSet.empty) C

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 VarMap.weaken {Γ : Context n m k} :
  VarMap Γ FinFun.weaken (Γ.var T) :=

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

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

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

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) :=

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)

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

structure TVarMap (Γ : 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 b, Γ.TBound X b -> Δ.TBound (f X) (b.trename f)
  cmap : ∀ c b, Γ.CBound c b -> Δ.CBound c b
  lmap : ∀ x S, Γ.LBound x S -> Δ.LBound x (S.trename f)

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

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

def Subcapt.weaken
  (h : Γ ⊢ C1 <:c C2) :
  (Γ,x: T) ⊢ C1.weaken <:c C2.weaken :=

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

def Subcapt.cweaken
  (h : Γ ⊢ C1 <:c C2) :
  (Γ.cvar b) ⊢ C1.cweaken <:c C2.cweaken :=

inductive Subcapt : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where
| trans :
  Subcapt Γ C1 C2 ->
  Subcapt Γ C2 C3 ->
  Subcapt Γ C1 C3
| subset :
  C1 ⊆ C2 ->
  Subcapt Γ C1 C2
| union :
  Subcapt Γ C1 C3 ->
  Subcapt Γ C2 C3 ->
  Subcapt Γ (C1 ∪ C2) C3
| var :
  Context.Bound Γ x (CType.capt C S) ->
  Subcapt Γ {x=x} C
| cinstl :
  Context.CBound Γ c (CBinding.inst C) ->
  Subcapt Γ C {c=c}
| cinstr :
  Context.CBound Γ c (CBinding.inst C) ->
  Subcapt Γ {c=c} C
| cbound :
  Context.CBound Γ c (CBinding.bound (CBound.upper C)) ->
  Subcapt Γ {c=c} C

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 EType.tweaken (E : EType n m k) : EType n (m+1) k :=
  E.trename FinFun.weaken

def CType.tweaken (C : CType n m k) : CType n (m+1) k :=
  C.trename 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 SType.IsVar : SType n m k -> Prop where
| tvar : SType.IsVar (SType.tvar X)

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 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

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}

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.tweaken : Cont n m k -> Cont n (m+1) k
| Cont.none => Cont.none
| Cont.cons t cont => Cont.cons t.tweaken cont.tweaken
| Cont.conse t cont => Cont.conse t.tweaken cont.tweaken
| Cont.scope x cont => Cont.scope x cont.tweaken

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

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

inductive ESubtyp : Context n m k -> EType n m k -> EType n m k -> Prop where
| exist :
  CSubtyp (Context.cvar Γ (CBinding.bound CBound.star)) T1 T2 ->
  ESubtyp Γ (EType.ex T1) (EType.ex T2)
| type :
  CSubtyp Γ T1 T2 ->
  ESubtyp Γ (EType.type T1) (EType.type T2)

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

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

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

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

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

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

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

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

def FinFun.id : FinFun n n :=
  fun i => i

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

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

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

Function.Injective in Init.Data.Function

inductive TypedState : State n m k -> Context n m k -> EType n m k -> Prop where
| mk :
  TypedStore σ Γ ->
  Typed Γ t E Ct ->
  WellScoped Γ cont Ct ->
  TypedCont Γ E cont E' C ->
  TypedState (State.mk σ cont t) Γ E'

def CVarMap.text {Γ : Context n m k} {Δ : Context n m k'}
  (ρ : CVarMap Γ f Δ) (b : TBinding n m k) :
  CVarMap (Γ.tvar b) f (Δ.tvar (b.crename f)) :=

def SSubtyp.dealias_cforall_inv.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {B1 E1 B2 E2}
    (ht : Γ.IsTight)
    (h1 : SType.Dealias Γ S1 (SType.cforall B1 E1))
    (h2 : SType.Dealias Γ S2 (SType.cforall B2 E2)),
    Subbound Γ B2 B1 ∧ ESubtyp (Γ.cvar (CBinding.bound B2)) E1 E2

def SSubtyp.csubst_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') (ρ : CVarSubst Γ f Δ),
  SSubtyp Δ (S1.crename f) (S2.crename f)

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

def CVarSubst.narrow
  (hs : Subbound Γ B' B) :
  CVarSubst
    (Γ,c<:B)
    FinFun.id
    (Γ,c<:B') :=

infix:30 "

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

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

def VarSubst.cext {Γ : Context n m k}
  (σ : VarSubst Γ f Δ) :
  VarSubst (Γ.cvar b) f (Δ.cvar (b.rename f)) :=

@[simp]
def CType.cweaken_capt :
  (CType.capt C S).cweaken = CType.capt C.cweaken S.cweaken :=

def FinFun.open (x : Fin n) : FinFun (n+1) n :=

Or.inr in Init.Prelude

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

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

structure VarSubst (Γ : Context n m k) (f : FinFun n n') (Δ : Context n' m k) where
  map : ∀ x E, Γ.Bound x E -> Typed Δ (Term.var (f x)) (EType.type (E.rename f)) {x=f x}
  tmap : ∀ X b, Γ.TBound X b -> Δ.TBound X (b.rename f)
  cmap : ∀ c b, Γ.CBound c b -> Δ.CBound c (b.rename f)
  lmap : ∀ l S, Γ.LBound l S -> Δ.LBound (f l) (S.rename 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)

Union in Init.Core

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

def VarSubst.text {Γ : Context n m k}
  (σ : VarSubst Γ f Δ) :
  VarSubst (Γ.tvar b) f (Δ.tvar (b.rename f)) :=

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

abs in Mathlib.Algebra.Order.Group.Unbundled.Abs
</all_available_defs>

<all_available_lemmas>
theorem SSubtyp.weaken
  (h : SSubtyp Γ S1 S2) :
  ∀ b, SSubtyp (Γ.var b) S1.weaken S2.weaken

theorem Subbound.weaken
  (h : Subbound Γ B1 B2) :
  Subbound (Γ.var b) B1.weaken B2.weaken

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

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

theorem SSubtyp.tweaken
  (h : SSubtyp Γ S1 S2) :
  SSubtyp (Γ.tvar b) S1.tweaken S2.tweaken

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

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

theorem Subbound.tweaken
  (h : Subbound Γ B1 B2) :
  Subbound (Γ.tvar b) B1 B2

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

theorem SSubtyp.cweaken
  (h : SSubtyp Γ S1 S2) :
  ∀ b, SSubtyp (Γ.cvar b) S1.cweaken S2.cweaken

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

theorem Subbound.cweaken
  (h : Subbound Γ B1 B2) :
  Subbound (Γ.cvar b) B1.cweaken B2.cweaken

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 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 SType.trename_rename_comm (S : SType n m k) (f : FinFun n n') (g : FinFun m m') :
  (S.trename g).rename f = (S.rename f).trename g

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

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

theorem SType.crename_trename_comm (S : SType n m k) (f : FinFun k k') (g : FinFun m m') :
  (S.crename f).trename g = (S.trename g).crename f

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

theorem Typed.tweaken_ext {Γ : Context n m k}
  (h : Typed (Γ.var T) t E Ct) :
  Typed ((Γ.tvar b).var T.tweaken) t.tweaken E.tweaken Ct

theorem Typed.tweaken_cext_ext {Γ : Context n m k}
  (h : Typed ((Γ.cvar (CBinding.bound B)).var T) t E Ct) :
  Typed (((Γ.tvar b).cvar (CBinding.bound B)).var T.tweaken) t.tweaken E.tweaken Ct

theorem CBound.cweaken_def {b : CBound n k} :
  b.cweaken = b.crename FinFun.weaken

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

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

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

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

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

theorem Context.cvar_bound_cvar_inst_inv {Γ : Context n m k}
  (hb : Context.CBound (Context.cvar Γ (CBinding.bound b0)) c (CBinding.inst C)) :
  ∃ c0 C0, c = c0.succ ∧ C = C0.cweaken ∧ Context.CBound Γ c0 (CBinding.inst C0)

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

theorem ESubtyp.type_inv_subcapt'
  (heq : E1 = EType.type (CType.capt C S))
  (h : ESubtyp Γ E E1) :
  ∃ C0 S0, E = EType.type (CType.capt C0 S0) ∧ Subcapt Γ C0 C

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

theorem CSubtyp.tsubst
  (h : CSubtyp Γ T1 T2)
  (σ : TVarSubst Γ f Δ) :
  CSubtyp Δ (T1.trename f) (T2.trename f)

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

theorem Typed.open
  (h : Typed (Γ,x: P) t E Ct)
  (hx : Typed Γ (Term.var x) (EType.type P) Cx) :
  Typed Γ (t.open x) (E.open x) (Ct.open x)

theorem EType.crename_id {E : EType n m k} :
  E.crename FinFun.id = E

theorem Context.var_lbound_succ_inv
  (hb : Context.LBound (Γ.var T) x.succ S) :
  ∃ S0, Context.LBound Γ x S0 ∧ S = S0.weaken

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

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 Subcapt.refl :
  Subcapt Γ C C

theorem EType.weaken_trename {E : EType n m k} :
  (E.trename f).weaken = E.weaken.trename f

theorem WellScoped.subcapt
  (hsc : WellScoped Γ cont C)
  (hs : Γ ⊢ C' <:c C) :
  WellScoped Γ cont C'

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 CaptureSet.rename_rename {C : CaptureSet n k} :
  (C.rename f).rename g = C.rename (g ∘ f)

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 Store.bound_label
  (hl : Store.LBound σ x S)
  (ht : TypedStore σ Γ) :
  Γ.LBound x S

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

theorem CSubtyp.csubst
  (h : CSubtyp Γ T1 T2)
  (σ : CVarSubst Γ f Δ) :
  CSubtyp Δ (T1.crename f) (T2.crename f)

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

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 EType.rename_rename (E : EType n m k) (f : FinFun n n') (g : FinFun n' n'') :
  (E.rename f).rename g = E.rename (g ∘ f)

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

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

theorem Context.label_tbound_inv'
  (he : Γ0 = Γ.label l)
  (hb : Context.TBound Γ0 X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.weaken

theorem Context.tinst_tbound_bound_inv
  (hb : Context.TBound (Γ.tvar (TBinding.inst P)) X (TBinding.bound S)) :
  ∃ X0 S0, Context.TBound Γ X0 (TBinding.bound S0)
    ∧ S = SType.tweaken S0
    ∧ X = X0.succ

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

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 Context.cvar_bound_var_inv
  (hb : Context.Bound (Context.cvar Γ b) x E) :
  ∃ E0, Context.Bound Γ x E0 ∧ E = E0.cweaken

theorem Typed.app_inv_capt'
  (he : t0 = Term.app x y)
  (ht : Typed Γ t0 E Ct) :
  Γ ⊢ ({x=x}∪{x=y}) <:c Ct

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

theorem Context.tvar_tbound_inv'
  (he1 : Γ0 = Γ.tvar p)
  (hb : Context.TBound Γ0 X0 b) :
  (X0 = 0 ∧ b = p.tweaken) ∨
  (∃ b0 X, Context.TBound Γ X b0 ∧ b = b0.tweaken ∧ X0 = (Fin.succ X))

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

theorem Context.label_lbound_succ_inv
  (hb : Context.LBound (Γ.label l) x.succ S) :
  ∃ S0, Context.LBound Γ x S0 ∧ S = S0.weaken

theorem Typed.label_inv
  (ht : Typed Γ (Term.var x) (EType.type T) Ct) (hb : Γ.LBound x S1) :
  ∃ S0, Γ.LBound x S0 ∧ (Γ ⊢ (Label[S0]^{x=x}) <: T)

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

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

theorem Typed.topen
  (h : Typed (Γ,X<: (SType.tvar X)) t E Ct) :
  Typed Γ (t.topen X) (E.topen X) Ct

theorem CType.tweaken_crename {C : CType n m k} :
  (C.crename f).tweaken = C.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 Context.tbound_tbound_inst_inv
  (hb : Context.TBound (Γ.tvar (TBinding.bound P)) X (TBinding.inst S)) :
  ∃ X0 S0, Context.TBound Γ X0 (TBinding.inst S0)
    ∧ S = SType.tweaken S0
    ∧ X = X0.succ

theorem Context.tvar_tbound_succ_inv
  (hb : Context.TBound (Γ.tvar p) (Fin.succ X) b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.tweaken

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

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

theorem Typed.boundary_inv' {Γ : Context n m k} {S : SType n m k}
  (he : t0 = (boundary:S in t))
  (ht : Typed Γ t0 E Ct) :
  Typed
    ((Γ,c<:*),x: Label[S.cweaken]^{c=0})
    t
    (S.cweaken.weaken^{})
    (Ct.cweaken.weaken ∪ {c=0} ∪ {x=0}) ∧
    (Γ ⊢ (S^{}) <:e E)

theorem Context.cvar_bound_cbound_inv_inst'
  (he : b = CBinding.inst C)
  (hb : Context.CBound (Γ,c<:B) c b) :
  ∃ c0 C0, Context.CBound Γ c0 (CBinding.inst C0)
    ∧ c = c0.succ
    ∧ C = C0.cweaken

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

theorem Store.val_lookup_exists {σ : Store n m k} {x : Fin n}
  (hs : TypedStore σ Γ) (hx : Typed Γ (Term.var x) (EType.type T) Cx)
  (hvt : T.IsValue) :
  ∃ v, Store.Bound σ x v ∧ v.IsValue

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

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

theorem Typed.bindc_inv {Γ : Context n m k}
  (h : Typed Γ (let c=C in t) E Ct) :
  ∃ E0,
    Typed (Γ,c:=C) t E0.cweaken Ct.cweaken ∧
    (Γ ⊢ E0 <:e E)

theorem CSubtyp.subst
  (h : CSubtyp Γ T1 T2)
  (σ : VarSubst Γ f Δ) :
  CSubtyp Δ (T1.rename f) (T2.rename f)

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

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

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

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 IsValue.crename_l {t : Term n m k}
  (hv : (t.crename f).IsValue) :
  t.IsValue

theorem EType.cweaken_rename_comm {E : EType n m k} :
  E.cweaken.rename f = (E.rename f).cweaken

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 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 CaptureSet.open_weaken_ext {C : CaptureSet (n+1) k} :
  (C.rename (FinFun.weaken.ext)).rename (FinFun.open 0) = C

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 CType.crename_crename (T : CType n m k) (f : FinFun k k') (g : FinFun k' k'') :
  (T.crename f).crename g = T.crename (g ∘ f)

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 Context.cvar_bound_cvar_inst_inv' {Γ : Context n m k}
  (he1 : Γ' = Context.cvar Γ (CBinding.bound b0))
  (he2 : b' = CBinding.inst C)
  (hb : Context.CBound Γ' c b') :
  ∃ c0 C0, c = c0.succ ∧ C = C0.cweaken ∧ Context.CBound Γ c0 (CBinding.inst C0)

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

theorem Context.bound_lbound_absurd
  (hb1 : Context.Bound Γ x T)
  (hb2 : Context.LBound Γ x S) : False

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

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

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

theorem CType.cweaken_rename_comm {C : CType n m k} :
  C.cweaken.rename f = (C.rename f).cweaken

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

theorem Context.tvar_tbound_succ_inv'
  (he1 : Γ0 = Γ.tvar p) (he2 : X0 = Fin.succ X)
  (hb : Context.TBound Γ0 X0 b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.tweaken

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

theorem Typed.letin_inv {Γ : Context n m k}
  (h : Typed Γ (Term.letin t u) E Ct) :
  ∃ T E0,
    Typed Γ t (EType.type T) Ct ∧
    Typed (Γ.var T) u E0.weaken Ct.weaken ∧
    ESubtyp Γ E0 E

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

theorem SSubtyp.dealias_right_label
  (h : SSubtyp Γ S1 S2) (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S2 (SType.label T2)) :
  ∃ T1, SType.Dealias Γ S1 (SType.label T1)

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

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

theorem Typed.var_inv_cs'
  (he1 : t0 = Term.var x)
  (he2 : E0 = EType.type (S^C))
  (hx : Typed Γ t0 E0 Cx) :
  Γ ⊢ ({x=x}) <:c C

theorem Context.label_tbound_inv_bound
  (hb : Context.TBound (Γ.label l) X (TBinding.bound S)) :
  ∃ S0, Context.TBound Γ X (TBinding.bound S0) ∧ S = SType.weaken S0

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

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

theorem Subcapt.tsubst
  (h : Subcapt Γ C1 C2)
  (σ : TVarSubst Γ f Δ) :
  Subcapt Δ C1 C2

theorem FinFun.weaken_inj {n : Nat} : Function.Injective (weaken (n := n))

theorem Term.trename_id {t : Term n m k} :
  t.trename FinFun.id = t

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 SType.cweaken_trename {S : SType n m k} :
  (S.trename f).cweaken = S.cweaken.trename f

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

@[simp]
lemma TBinding.cweaken_bound: (TBinding.bound T).cweaken = TBinding.bound (T.cweaken)

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

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

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

theorem Typed.precise_cv'
  (he : t0 = Term.var x)
  (h : Typed Γ t0 E C0) :
  Typed Γ (Term.var x) E {x=x}

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

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

theorem Typed.precise_cv
  (h : Typed Γ (Term.var x) E C0) :
  Typed Γ (Term.var x) E {x=x}

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

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

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 Typed.var_inv_cs
  (hx : Typed Γ (Term.var x) (EType.type (S^C)) Cx) :
  Γ ⊢ ({x=x}) <:c C

@[simp]
lemma TBinding.cweaken_inst: (TBinding.inst T).cweaken = TBinding.inst (T.cweaken)

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

theorem WellScoped.cweaken
  (h : WellScoped Γ E Ct) :
  WellScoped (Γ.cvar b) E.cweaken Ct.cweaken

theorem Context.cvar_tbound_inv'
  (he : Γ0 = Γ.cvar p)
  (hb : Context.TBound Γ0 X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.cweaken

theorem Typed.label_inv_sub
  (ht : Typed Γ (Term.var x) (Label[S]^C) Ct) (hb : Γ.LBound x S1)
  (hg : Γ.IsTight) :
  ∃ S0, Γ.LBound x S0 ∧ (Γ ⊢ S <:s S0)

theorem Context.tinst_tbound_bound_inv'
  (he1 : Γ0 = Γ.tvar (TBinding.inst P))
  (he2 : b0 = TBinding.bound S)
  (hb : Context.TBound Γ0 X b0) :
  ∃ X0 S0, Context.TBound Γ X0 (TBinding.bound S0)
    ∧ S = SType.tweaken S0
    ∧ X = X0.succ

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

theorem Context.cvar_cbound_succ_inv
  (hb : Context.CBound (Γ.cvar p) (Fin.succ X) b) :
  ∃ b0, Context.CBound Γ X b0 ∧ b = b0.cweaken

theorem CType.weaken_crename {C : CType n m k} :
  (C.crename f).weaken = C.weaken.crename f

lemma CBinding.crename_inst: (CBinding.inst T).crename f = CBinding.inst (T.crename f)
</all_available_lemmas>

<local_ctx>
import Capless.Store

import Capless.Weakening.Typing

import Capless.Weakening.Subtyping

import Capless.Weakening.Subcapturing

namespace Capless
</local_ctx>

<target_theorem>
theorem WellScoped.tweaken
  (h : WellScoped Γ cont Ct) :
  WellScoped (Γ.tvar b) cont.tweaken Ct :=
</target_theorem>

