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:
* <used_lib_defs>...</used_lib_defs>: Imported library definitions directly used by the theorem.
* <used_repo_defs>...</used_repo_defs>: Definitions from the local project (but outside the current file), directly or transitively used by the theorem.
* <lib_lemmas>...</lib_lemmas>: Imported library lemmas/theorems that may assist the proof.
* <repo_lemmas>...</repo_lemmas>: Lemmas/theorems defined in the local project outside this file.
* <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 used definitions and helpful lemmas (used_lib_defs, used_repo_defs, lib_lemmas, repo_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:
<used_lib_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)
</used_lib_defs>

<repo_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]
</repo_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:
<used_lib_defs>
Nat in Init.Prelude
Fin in Init.Prelude
Fin.succ in Init.Data.Fin.Basic
abs in Mathlib.Algebra.Order.Group.Unbundled.Abs
</used_lib_defs>

<used_repo_defs>
notation:50 "λ[X<:" S "]" t => Term.tlam S t

notation:40 "let" "x=" t " in " u => Term.letin t u

notation:40 "let" "(c,x)=" t " in " u => Term.letex t u

notation:40 "let" "X=" S " in " t => Term.bindt S t

notation:40 "let" "c=" C " in " t => Term.bindc C t

notation:50 "λ(x:" T ")" t => Term.lam T t

notation:50 "λ[c<:" B "]" t => Term.clam B t

notation:max "{x=" x "}" => CaptureSet.singleton x

notation:max "{c=" c "}" => CaptureSet.csingleton c

notation:50 Γ " ⊢ " E1 " <:e " E2 => ESubtyp Γ E1 E2

notation:50 Γ " ⊢ " T1 " <:s " T2 => SSubtyp Γ T1 T2

notation:50 Γ " ⊢ " T1 " <: " T2 => CSubtyp Γ T1 T2

notation:40 Γ " ⊢ " t:80 " : " E " @ " C => Typed Γ t E C

notation:50 Γ " ⊢ " C1 " <:c " C2 => Subcapt Γ C1 C2

notation:40 "Label[" S "]" => SType.label S

notation:60 "□" T => SType.box T

notation:30 Γ ",c:=" C => Context.cvar Γ (CBinding.inst C)

notation:50 "∀(x:" T ")" U => SType.forall T U

notation:50 "∀[c<:" B "]" T => SType.cforall B T

notation:30 Γ ",c<:" B => Context.cvar Γ (CBinding.bound B)

notation:30 Γ ",X<:" T => Context.tvar Γ (TBinding.bound T)

notation:30 Γ ",X:=" T => Context.tvar Γ (TBinding.inst T)

notation:30 Γ ",x:" T => Context.var Γ T

notation:30 Γ ",c<:*" => Context.cvar Γ (CBinding.bound CBound.star)

notation:50 "∀[X<:" S "]" T => SType.tforall S T

notation:40 "∃c." T => EType.ex T

notation:40 "boundary:" S " in " t => Term.boundary S t

macro "easy" : tactic => `(tactic| assumption)

notation:max "⟨" σ " | " cont " | " t "⟩" => State.mk σ cont t

macro "apply!" e:term : tactic => `(tactic| apply $e <;> easy)

macro "apply?" e:term : tactic => `(tactic| apply $e <;> try easy)

macro "split_and" : tactic => `(tactic| repeat any_goals apply And.intro)

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

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

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

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

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)

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

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)

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)

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)

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

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

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

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

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

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 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 FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) :=

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

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)

@[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 FinFun.weaken : FinFun n (n+1) :=
  Fin.succ

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)

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)

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)

inductive Subbound : Context n m k -> CBound n k -> CBound n k -> Prop where
| set :
  (Γ ⊢ C1 <:c C2) ->
  Subbound Γ (CBound.upper C1) (CBound.upper C2)
| star :
  Subbound Γ B CBound.star

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

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

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

@[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}

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

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

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

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 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 Typed.cweaken
  (h : Typed Γ t E Ct) :
  Typed (Γ.cvar b) t.cweaken E.cweaken Ct.cweaken :=

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

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 CVarMap.weaken {Γ : Context n m k} :
  CVarMap Γ FinFun.weaken (Γ.cvar b) :=

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

inductive Reduce : State n m k -> State n' m' k' -> Prop where
| apply {σ : Store n m k} :
  σ.Bound x (Term.lam T t) ->
  Reduce ⟨σ | cont | Term.app x y⟩ ⟨σ | cont | t.open y⟩
| tapply {σ : Store n m k} :
  σ.Bound x (Term.tlam S t) ->
  Reduce ⟨σ | cont | Term.tapp x X⟩ ⟨σ | cont | t.topen X⟩
| capply {σ : Store n m k} :
  σ.Bound x (Term.clam B t) ->
  Reduce ⟨σ | cont | Term.capp x c⟩ ⟨σ | cont | t.copen c⟩
| enter :
  Reduce
    ⟨σ | cont | boundary:S in t⟩
    ⟨(σ.label S).cval {x=0} | cont.weaken.cweaken.scope 0 | t⟩
| leave_var :
  Reduce
    ⟨σ | cont.scope x | Term.var y⟩
    ⟨σ | cont | Term.var y⟩
| leave_val {v : Term n m k} :
  (hv : Term.IsValue v) ->
  Reduce
    ⟨σ | cont.scope x | v⟩
    ⟨σ | cont | v⟩
| invoke {σ : Store n m k} {cont : Cont n m k} :
  σ.LBound x S ->
  cont.HasLabel x tail ->
  Reduce
    ⟨σ | cont | Term.invoke x y⟩
    ⟨σ | tail | Term.var y⟩
| push :
  Reduce
    ⟨σ | cont | Term.letin t u⟩
    ⟨σ | Cont.cons u cont | t⟩
| push_ex :
  Reduce
    ⟨σ | cont | Term.letex t u⟩
    ⟨σ | Cont.conse u cont | t⟩
| rename :
  Reduce
    ⟨σ | Cont.cons u cont | Term.var x⟩
    ⟨σ | cont | u.open x⟩
| lift :
  (hv : Term.IsValue v) ->
  Reduce
    ⟨σ | Cont.cons u cont | v⟩
    ⟨σ.val v hv | cont.weaken | u⟩
| lift_ex :
  Reduce
    ⟨σ | Cont.conse u cont | Term.pack C x⟩
    ⟨σ.cval C | cont.cweaken | u.open x⟩
| tlift :
  Reduce
    ⟨σ | cont | Term.bindt S t⟩
    ⟨σ.tval S | cont.tweaken | t⟩
| clift :
  Reduce
    ⟨σ | cont | Term.bindc C t⟩
    ⟨σ.cval C | cont.cweaken | t⟩

infix:30 " 

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

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

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

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 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 TVarMap.weaken {Γ : Context n m k} :
  TVarMap Γ FinFun.weaken (Γ.tvar b) :=

inductive SType.IsVar : SType n m k -> Prop where
| tvar : SType.IsVar (SType.tvar X)

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

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

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

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

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

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

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

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

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

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 CaptureSet.weaken1 (C : CaptureSet (n+1) k) : CaptureSet (n+2) k :=
  C.rename FinFun.weaken.ext

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

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

def VarSubst.narrow
  (hs : CSubtyp Γ T' T) :
  VarSubst (Γ.var T) FinFun.id (Γ.var T') :=

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 FinFun.id : FinFun n n :=
  fun i => i

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

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

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

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

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

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

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

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

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

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

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

def CVarSubst.open :
  CVarSubst
    (Γ.cvar (CBinding.bound (CBound.upper {c=c})))
    (FinFun.open c)
    Γ :=

structure CVarSubst (Γ : 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 C, Γ.CBound c (CBinding.inst C) ->
    Δ.CBound (f c) (CBinding.inst (C.crename f))
  cmap_bound : ∀ c B, Γ.CBound c (CBinding.bound B) ->
    Subbound Δ (CBound.upper {c=f c}) (B.crename f)
  lmap : ∀ l S, Γ.LBound l S -> Δ.LBound l (S.crename f)

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

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

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

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

def CaptureSet.open (C : CaptureSet (n+1) k) (x : Fin n) : CaptureSet n 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)

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

def TVarSubst.open :
  TVarSubst
    (Γ.tvar (TBinding.bound (SType.tvar X)))
    (FinFun.open X)
    Γ :=
  { map := fun x E hb => by admit /- proof elided -/

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 TVarSubst.narrow
  (hs : SSubtyp Γ S' S) :
  TVarSubst
    (Γ.tvar (TBinding.bound S))
    FinFun.id
    (Γ.tvar (TBinding.bound S')) :=

def VarSubst.open
  (hx : Typed Γ (Term.var x) (EType.type T) Cx) :
  VarSubst (Γ.var T) (FinFun.open x) Γ :=

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

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

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

def Typed.cweaken_cext_ext {Γ : Context n m k}
  (h : Typed ((Γ.cvar (CBinding.bound B)).var T) t E Ct) :
  Typed (((Γ.cvar b).cvar (CBinding.bound B.cweaken)).var T.cweaken1) t.cweaken1 E.cweaken1 Ct.cweaken1 :=

def CVarMap.weaken_cext_ext {Γ : Context n m k} :
  CVarMap
    ((Γ.cvar (CBinding.bound B)).var T)
    FinFun.weaken.ext
    (((Γ.cvar b).cvar (CBinding.bound B.cweaken)).var T.cweaken1) :=

def CVarMap.cext {Γ : Context n m k} {Δ : Context n m k'}
  (ρ : CVarMap Γ f Δ) (b : CBinding n k) :
  CVarMap (Γ.cvar b) f.ext (Δ.cvar (b.crename 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 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 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 CVarMap.ext {Γ : Context n m k} {Δ : Context n m k'}
  (ρ : CVarMap Γ f Δ) (E : CType n m k) :
  CVarMap (Γ.var E) f (Δ.var (E.crename f)) :=

def Typed.cweaken_ext {Γ : Context n m k}
  (h : Typed (Γ.var T) t E Ct) :
  Typed ((Γ.cvar b).var T.cweaken) t.cweaken E.cweaken Ct.cweaken :=

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

def VarMap.weaken_ext {Γ : Context n m k} :
  VarMap
    (Γ.var T)
    FinFun.weaken.ext
    ((Γ.var P).var T.weaken) :=

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

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 VarMap.cext {Γ : Context n m k} {Δ : Context n' m k}
  (ρ : VarMap Γ f Δ) (b : CBinding n k) :
  VarMap (Γ.cvar b) f (Δ.cvar (b.rename f)) :=

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

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.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 TVarMap.cext {Γ : Context n m k} {Δ : Context n m' k}
  (ρ : TVarMap Γ f Δ) (b : CBinding n k) :
  TVarMap (Γ.cvar b) f (Δ.cvar b) :=

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

def SType.copen (S : SType n m (k+1)) (x : Fin k) : SType n m k :=
  S.crename (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 EType.copen (E : EType n m (k+1)) (x : Fin k) : EType n m k :=
  E.crename (FinFun.open x)

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

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

def Term.topen (t : Term n (m+1) k) (X : Fin m) : Term n m k :=
  t.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 CVarRename.boundary {Γ : Context n m k} {S : SType n m k} :
  CVarMap
    (((Γ.label S),c<:*),x:(Label[S.weaken.cweaken])^{c=0})
    FinFun.weaken.ext
    ((((Γ.label S),c:={x=0}),c<:*),x:(Label[S.weaken.cweaken.cweaken])^{c=0}) :=

@[simp]
def CType.weaken_capt :
  (CType.capt C S).weaken = CType.capt C.weaken S.weaken :=

def VarRename.boundary {Γ : Context n m k} {S : SType n m k} :
  VarMap
    ((Γ,c<:*),x:(Label[S.cweaken])^{c=0})
    FinFun.weaken.ext
    (((Γ.label S),c<:*),x:(Label[S.weaken.cweaken])^{c=0}) :=

def CVarSubst.boundary {Γ : Context n m k} {S : SType n m k} :
  CVarSubst
    ((((Γ.label S),c:={x=0}),c<:*),x:(Label[S.weaken.cweaken.cweaken])^{c=0})
    (FinFun.open 0)
    (((Γ.label S),c:={x=0}),x:(Label[S.weaken.cweaken])^{c=0}) :=

def VarSubst.boundary {Γ : Context n m k} {S : SType n m k} :
  VarSubst
    (((Γ.label S),c:={x=0}),x:(Label[S.weaken.cweaken])^{c=0})
    (FinFun.open 0)
    ((Γ.label S),c:={x=0}) :=

def CVarSubst.text {Γ : Context n m k}
  (σ : CVarSubst Γ f Δ) :
  CVarSubst (Γ.tvar T) f (Δ.tvar (T.crename f)) :=

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

inductive Store.TBound : Store n m k -> (Fin m) -> SType n m k -> Prop where
| here :
  Store.TBound (Store.tval σ S) 0 S.tweaken
| there_val :
  Store.TBound σ x S ->
  Store.TBound (Store.val σ t hv) x S.weaken
| there_tval :
  Store.TBound σ x S ->
  Store.TBound (Store.tval σ S') (Fin.succ x) S.tweaken
| there_cval :
  Store.TBound σ x S ->
  Store.TBound (Store.cval σ C) x S.cweaken
| there_label :
  Store.TBound σ x S ->
  Store.TBound (Store.label σ S') x S.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 CVarSubst.ext {Γ : Context n m k}
  (σ : CVarSubst Γ f Δ)
  (T : CType n m k) :
  CVarSubst (Γ.var T) f (Δ.var (T.crename f)) :=

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

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

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.crename_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') (ρ : CVarMap Γ f Δ),
  ESubtyp Δ (E1.crename f) (E2.crename f)

inductive SType.IsValue : SType n m k -> Prop where
| xforall : SType.IsValue (∀(x:T)U)
| tforall : SType.IsValue (∀[X<:S]T)
| cforall : SType.IsValue (∀[c<:B]T)
| box : SType.IsValue (□ T)

@[aesop safe [constructors, cases]]

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 VarMap.text {Γ : Context n m k} {Δ : Context n' m k}
  (ρ : VarMap Γ f Δ) (b : TBinding n m k) :
  VarMap (Γ.tvar b) f (Δ.tvar (b.rename f)) :=

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

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

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

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

def SSubtyp.trename_motive2
  (Γ : Context n m k)
  (T1 : CType n m k)
  (T2 : CType n m k)
  : Prop :=
  ∀ {m'} (f : FinFun m m') (Δ : Context n m' k) (ρ : TVarMap Γ f Δ),
  CSubtyp Δ (T1.trename f) (T2.trename f)

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

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

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)

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)

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 EType.rename_open :
  (EType.open E x).rename f = (E.rename f.ext).open (f x) :=

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

def CVarSubst.cext {Γ : Context n m k}
  (σ : CVarSubst Γ f Δ) :
  CVarSubst (Γ.cvar b) f.ext (Δ.cvar (b.crename f)) :=

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

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

def VarMap.lweaken_ext {Γ : Context n m k} :
  VarMap
    (Γ.var T)
    FinFun.weaken.ext
    ((Γ.label P).var T.weaken) :=

def VarMap.lweaken {Γ : Context n m k} :
  VarMap Γ FinFun.weaken (Γ.label S) :=

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 CVarSubst.instantiate {Γ : Context n m k} :
  CVarSubst
    (Γ.cvar (CBinding.bound CBound.star))
    FinFun.id
    (Γ.cvar (CBinding.inst C)) :=

@[simp]
def CBound.cweaken_upper :
  (CBound.upper C).cweaken = CBound.upper C.cweaken :=

inductive SType.Dealias : Context n m k -> SType n m k -> SType n m k -> Prop where
| refl :
  Dealias Γ S S
| step :
  Context.TBound Γ X (TBinding.inst S) ->
  Dealias Γ S S' ->
  Dealias Γ (SType.tvar X) S'

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

notation:50 "λ(x:" T ")" t => Term.lam T t

notation:50 "λ[X<:" S "]" t => Term.tlam S t

notation:50 "λ[c<:" B "]" t => Term.clam B t

notation:40 "let" "x=" t " in " u => Term.letin t u

notation:40 "let" "(c,x)=" t " in " u => Term.letex t u

notation:40 "let" "X=" S " in " t => Term.bindt S t

notation:40 "let" "c=" C " in " t => Term.bindc C t

notation:40 "boundary:" S " in " t => Term.boundary S t

notation:max "{x=" x "}" => CaptureSet.singleton x

notation:max "{c=" c "}" => CaptureSet.csingleton c

notation:50 Γ " ⊢ " E1 " <:e " E2 => ESubtyp Γ E1 E2

notation:50 Γ " ⊢ " T1 " <:s " T2 => SSubtyp Γ T1 T2

notation:50 Γ " ⊢ " T1 " <: " T2 => CSubtyp Γ T1 T2

notation:30 Γ ",x:" T => Context.var Γ T

notation:30 Γ ",X<:" T => Context.tvar Γ (TBinding.bound T)

notation:30 Γ ",X:=" T => Context.tvar Γ (TBinding.inst T)

notation:30 Γ ",c<:" B => Context.cvar Γ (CBinding.bound B)

notation:30 Γ ",c<:*" => Context.cvar Γ (CBinding.bound CBound.star)

notation:30 Γ ",c:=" C => Context.cvar Γ (CBinding.inst C)

notation:40 Γ " ⊢ " t:80 " : " E " @ " C => Typed Γ t E C

notation "⊤" => SType.top

notation:50 "∀(x:" T ")" U => SType.forall T U

notation:50 "∀[X<:" S "]" T => SType.tforall S T

notation:50 "∀[c<:" B "]" T => SType.cforall B T

notation:max S " ^ " C => CType.capt C S

notation:40 "∃c." T => EType.ex T

notation:40 "Label[" S "]" => SType.label S

notation:60 "□" T => SType.box T

notation:50 Γ " ⊢ " C1 " <:c " C2 => Subcapt Γ C1 C2
</used_repo_defs>

<repo_lemmas>
theorem Subcapt.refl :
  Subcapt Γ C C

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

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

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

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

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

theorem TypedCont.cweaken
  (h : TypedCont Γ E t E' Ct) :
  TypedCont (Γ.cvar b) E.cweaken t.cweaken E'.cweaken Ct.cweaken

theorem Cont.HasLabel.cweaken
  (h : Cont.HasLabel cont l tail) :
  Cont.HasLabel (cont.cweaken) l tail.cweaken

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

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

theorem CaptureSet.cweaken1_weaken (C : CaptureSet n (k+1)) :
  C.weaken.cweaken1 = C.cweaken1.weaken

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

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

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

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

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

theorem WellScoped.weaken
  (h : WellScoped Γ cont Ct) :
  WellScoped (Γ.var T) cont.weaken Ct.weaken

theorem Cont.HasLabel.weaken
  (h : Cont.HasLabel cont x tail) :
  Cont.HasLabel cont.weaken x.succ tail.weaken

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

theorem CaptureSet.weaken_cweaken (C : CaptureSet n k) :
  C.cweaken.weaken = C.weaken.cweaken

theorem CaptureSet.weaken1_weaken (C : CaptureSet n k) :
  C.weaken.weaken1 = C.weaken.weaken

theorem EType.weaken_ex (T : CType n m (k+1)) :
  (EType.ex T).weaken = EType.ex T.weaken

theorem EType.weaken1_weaken (E : EType n m k) :
  E.weaken.weaken1 = E.weaken.weaken

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

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

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

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

theorem Typed.narrow
  (h : Typed (Γ,x: T) t E Ct)
  (hs : CSubtyp Γ T' T) :
  Typed (Γ,x: T') t E Ct

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

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

theorem CaptureSet.crename_id {C : CaptureSet n k} :
  C.crename FinFun.id = C

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

theorem Typed.capp_inv
  (h : Typed Γ (Term.capp x c) E Ct0) :
  ∃ Cf F E0,
    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall (CBound.upper {c=c}) F))) {x=x} ∧
    E0 = F.copen c ∧
    ESubtyp Γ E0 E

theorem Typed.capp_inv'
  (he : t0 = Term.capp x c)
  (h : Typed Γ t0 E Ct0) :
  ∃ Cf F E0,
    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall (CBound.upper {c=c}) F))) {x=x} ∧
    E0 = F.copen c ∧
    ESubtyp Γ E0 E

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 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 Typed.val_precise_cv
  (ht : Typed Γ t (EType.type T) Ct)
  (hv : t.IsValue) :
  Typed Γ t (EType.type T) {}

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

theorem Typed.boundary_body_typing {Γ : Context n m k} {S : SType n m k}
  (ht : Typed ((Γ,c<:*),x:(Label[S.cweaken])^{c=0}) t E Ct) :
  Typed ((Γ.label S),c:={x=0}) t E Ct

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

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

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

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

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

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

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

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 CSubtyp.crename
  (h : CSubtyp Γ C1 C2)
  (ρ : CVarMap Γ f Δ) :
  CSubtyp Δ (C1.crename f) (C2.crename f)

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

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

theorem ESubtyp.crename
  (h : ESubtyp Γ E1 E2)
  (ρ : CVarMap Γ f Δ) :
  ESubtyp Δ (E1.crename f) (E2.crename f)

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

theorem Subcapt.crename
  (h : Subcapt Γ C1 C2)
  (ρ : CVarMap Γ f Δ) :
  Subcapt Δ (C1.crename f) (C2.crename 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 CSubtyp.trename
  (h : CSubtyp Γ T1 T2)
  (ρ : TVarMap Γ f Δ) :
  CSubtyp Δ (T1.trename f) (T2.trename f)

theorem SSubtyp.trename
  (h : SSubtyp Γ S1 S2)
  (ρ : TVarMap Γ f Δ) :
  SSubtyp Δ (S1.trename f) (S2.trename f)

theorem ESubtyp.trename
  (h : ESubtyp Γ E1 E2)
  (ρ : TVarMap Γ f Δ) :
  ESubtyp Δ (E1.trename f) (E2.trename f)

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

theorem Subcapt.trename
  (h : Subcapt Γ C1 C2)
  (ρ : TVarMap Γ f Δ) :
  Subcapt Δ C1 C2

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 CSubtyp.rename
  (h : CSubtyp Γ T1 T2)
  (ρ : VarMap Γ f Δ) :
  CSubtyp Δ (T1.rename f) (T2.rename f)

theorem SSubtyp.rename
  (h : SSubtyp Γ S1 S2)
  (ρ : VarMap Γ f Δ) :
  SSubtyp Δ (S1.rename f) (S2.rename f)

theorem Subbound.rename
  (h : Subbound Γ B1 B2)
  (ρ : VarMap Γ f Δ) :
  Subbound Δ (B1.rename f) (B2.rename f)

theorem ESubtyp.rename
  (h : ESubtyp Γ E1 E2)
  (ρ : VarMap Γ f Δ) :
  ESubtyp Δ (E1.rename f) (E2.rename f)

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

theorem Subcapt.rename
  (h : Subcapt Γ C1 C2)
  (ρ : VarMap Γ f Δ) :
  Subcapt Δ (C1.rename f) (C2.rename f)

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

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.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 WellScoped.scope
  (hsc : WellScoped Γ cont C) :
  WellScoped Γ (Cont.scope x cont) C

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 Typed.letin_inv' {Γ : Context n m k}
  (he : t0 = Term.letin t u)
  (h : Typed Γ t0 E Ct0) :
  ∃ T E0,
    Typed Γ t (EType.type T) Ct0 ∧
    Typed (Γ.var T) u E0.weaken Ct0.weaken ∧
    ESubtyp Γ E0 E

theorem Cont.HasLabel.tweaken
  (h : Cont.HasLabel cont x tail) :
  Cont.HasLabel cont.tweaken x tail.tweaken

theorem TypedCont.lweaken
  (h : TypedCont Γ E cont E' Ct) :
  TypedCont (Γ.label S) E.weaken cont.weaken E'.weaken Ct.weaken

theorem Cont.HasLabel.lweaken
  (h : Cont.HasLabel cont x tail) :
  Cont.HasLabel cont.weaken x.succ tail.weaken

theorem WellScoped.lweaken
  (h : WellScoped Γ cont Ct) :
  WellScoped (Γ.label S) cont.weaken Ct.weaken

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

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

theorem SType.rename_rename (S : SType n m k) (f : FinFun n n') (g : FinFun n' n'') :
  (S.rename f).rename g = S.rename (g ∘ f)

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

theorem CaptureSet.rename_id {C : CaptureSet n k} :
  C.rename FinFun.id = C

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

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

theorem TypedCont.tweaken
  (h : TypedCont Γ E t E' C0) :
  TypedCont (Γ.tvar S) E.tweaken t.tweaken E'.tweaken C0

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

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

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

theorem Typed.bindt_inv {Γ : Context n m k}
  (h : Typed Γ (let X=T in t) E Ct) :
  ∃ E0,
    Typed (Γ,X:=T) t E0.tweaken Ct ∧
    (Γ ⊢ E0 <:e E)

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 CSubtyp.refl :
  CSubtyp Γ T T

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 Typed.csubst
  {Γ : Context n m k} {Δ : Context n m k'}
  (h : Typed Γ t E Ct)
  (σ : CVarSubst Γ f Δ) :
  Typed Δ (t.crename f) (E.crename f) (Ct.crename f)

theorem Typed.tapp_inv_capt
  (ht : Typed Γ (Term.tapp x X) E Ct) :
  Γ ⊢ ({x=x}) <:c Ct

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

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

theorem Typed.boundary_inv {Γ : Context n m k} {S : SType n m k}
  (ht : Typed Γ (boundary:S in t) 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 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 EType.rename_id {E : EType n m k} :
  E.rename FinFun.id = E

theorem CType.rename_id {T : CType n m k} :
  T.rename FinFun.id = T

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

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

theorem TypedCont.narrow
  (h : TypedCont Γ E1 cont E C0)
  (hsub : ESubtyp Γ E2 E1) :
  TypedCont Γ E2 cont E C0

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

theorem Typed.capp_inv_capt'
  (he : t0 = Term.capp x c)
  (ht : Typed Γ t0 E Ct) :
  Γ ⊢ ({x=x}) <:c 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 Typed.subst
  {Γ : Context n m k} {Δ : Context n' m k}
  (h : Typed Γ t E Ct)
  (σ : VarSubst Γ f Δ) :
  Typed Δ (t.rename f) (E.rename f) (Ct.rename f)

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 Typed.letex_inv' {Γ : Context n m k}
  (he : t0 = Term.letex t u)
  (h : Typed Γ t0 E Ct0) :
  ∃ T E0,
    Typed Γ t (EType.ex T) Ct0 ∧
    Typed ((Γ.cvar (CBinding.bound CBound.star)).var T) u E0.cweaken.weaken Ct0.cweaken.weaken ∧
    ESubtyp Γ E0 E

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 Typed.app_inv'
  (he : t0 = Term.app x y)
  (h : Typed Γ t0 E Ct0) :
  ∃ 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 Typed.precise_cv
  (h : Typed Γ (Term.var x) E C0) :
  Typed Γ (Term.var x) E {x=x}

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

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 Typed.canonical_form_clam'
  (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S0 (SType.cforall B' E))
  (he1 : t0 = Term.clam B t)
  (he2 : E0 = EType.type (CType.capt Cf S0))
  (h : Typed Γ t0 E0 Ct0) :
  Subbound Γ B' B ∧ Typed (Γ.cvar (CBinding.bound B')) t E Cf.cweaken

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

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 Store.bound_type
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ) :
  ∃ T0, Context.Bound Γ x T0

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

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

theorem Typed.copen
  (h : Typed (Γ,c<:CBound.upper {c=c}) t E Ct) :
  Typed Γ (t.copen c) (E.copen c) (Ct.copen c)

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

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

theorem CType.crename_rename_comm (C : CType n m k) (f : FinFun n n') (g : FinFun k k') :
  (C.rename f).crename g = (C.crename g).rename f

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

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 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 Typed.label_inv'
  (he1 : t0 = Term.var x)
  (he2 : E0 = EType.type T)
  (ht : Typed Γ t0 E0 Ct) (hb : Γ.LBound x S1) :
  ∃ S0, Γ.LBound x S0 ∧ (Γ ⊢ (Label[S0]^{x=x}) <: T)

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

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

theorem WellScoped.subset
  (hsc : WellScoped Γ cont C)
  (hs : C' ⊆ C) :
  WellScoped Γ cont C'

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

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

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

theorem ESubtyp.refl :
  ESubtyp Γ E E

theorem Typed.canonical_form_lam
  (ht : Γ.IsTight)
  (h : Typed Γ (Term.lam T t) (EType.type ((∀(x:T')E)^Cf)) Ct) :
  CSubtyp Γ T' T ∧
  Typed (Γ.var T') t E (Cf.weaken ∪ {x=0})

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 Typed.canonical_form_tlam
  (ht : Γ.IsTight)
  (h : Typed Γ (Term.tlam S t) (EType.type ((∀[X<:S']E)^Cf)) Ct0) :
  SSubtyp Γ S' S ∧
  Typed (Γ,X<:S') t E Cf

theorem Typed.canonical_form_tlam'
  (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S0 (SType.tforall S' E))
  (he1 : t0 = Term.tlam S t)
  (he2 : E0 = EType.type (CType.capt Cf S0))
  (h : Typed Γ t0 E0 Ct0) :
  SSubtyp Γ S' S ∧
  Typed (Γ.tvar (TBinding.bound S')) t E Cf

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 Typed.bindc_inv' {Γ : Context n m k}
  (he : t0 = Term.bindc C t)
  (h : Typed Γ t0 E Ct) :
  ∃ E0,
    Typed (Γ.cvar (CBinding.inst C)) t E0.cweaken Ct.cweaken ∧
    ESubtyp Γ E0 E

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

theorem Store.bound_label
  (hl : Store.LBound σ x S)
  (ht : TypedStore σ Γ) :
  Γ.LBound x S

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

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

<local_ctx>
import Capless.Store

import Capless.Type

import Capless.Reduction

import Capless.Inversion.Typing

import Capless.Inversion.Lookup

import Capless.Renaming.Term.Subtyping

import Capless.Renaming.Type.Subtyping

import Capless.Renaming.Capture.Subtyping

import Capless.Subst.Term.Typing

import Capless.Subst.Type.Typing

import Capless.Subst.Capture.Typing

import Capless.Weakening.TypedCont

import Capless.Tactics

import Capless.WellScoped.Basic

import Capless.Narrowing.TypedCont

import Capless.Typing.Boundary

namespace Capless

inductive Preserve : Context n m k -> EType n m k -> State n' m' k' -> Prop where
| mk :
  TypedState state Γ E ->
  Preserve Γ E state
| mk_weaken :
  TypedState state (Γ.var P) E.weaken ->
  Preserve Γ E state
| mk_tweaken :
  TypedState state (Γ.tvar b) E.tweaken ->
  Preserve Γ E state
| mk_cweaken :
  TypedState state (Γ.cvar b) E.cweaken ->
  Preserve Γ E state
| mk_enter :
  TypedState state ((Γ.label S).cvar b) E.weaken.cweaken ->
  Preserve Γ E state
</local_ctx>

<target_theorem>
theorem preservation
  (hr : Reduce state state')
  (ht : TypedState state Γ E) :
  Preserve Γ E state' :=
</target_theorem>

