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

def Term.open (t : Term (n+1) m k) (x : Fin n) : Term n m k :=
  t.rename (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 Term.copen (t : Term n m (k+1)) (c : Fin k) : Term n m k :=
  t.crename (FinFun.open c)

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 " 

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 SSubtyp.csubst_motive1
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop :=
  ∀ {k'} (f : FinFun k k') (Δ : Context n m k') (ρ : CVarSubst Γ f Δ),
  ESubtyp Δ (E1.crename f) (E2.crename f)

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

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)

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

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

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

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]
instance : HasSubset (CaptureSet n k) where
  Subset := CaptureSet.Subset

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

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

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

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

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

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

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

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

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

def EType.rename_open :
  (EType.open E x).rename f = (E.rename f.ext).open (f x) :=

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 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 FinFun (n n' : Nat) : Type :=
  Fin n -> Fin n'

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

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

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

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

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

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

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

def SSubtyp.subst_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) (ρ : VarSubst Γ f Δ),
  ESubtyp Δ (E1.rename f) (E2.rename f)

def SSubtyp.subst_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) (ρ : VarSubst Γ f Δ),
  CSubtyp Δ (C1.rename f) (C2.rename f)

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

def SSubtyp.tsubst_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) (ρ : TVarSubst Γ f Δ),
  ESubtyp Δ (E1.trename f) (E2.trename f)

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

def SSubtyp.tsubst_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) (ρ : TVarSubst Γ f Δ),
  SSubtyp Δ (S1.trename f) (S2.trename f)

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

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

instance : Coe (CType n m k) (EType n m k) where
  coe T := EType.type 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)

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)

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 VarSubst.ext {Γ : Context n m k}
  (σ : VarSubst Γ f Δ)
  (T : CType n m k) :
  VarSubst (Γ.var T) f.ext (Δ.var (T.rename f)) :=

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

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

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

def TVarSubst.ext {Γ : Context n m k}
  (σ : TVarSubst Γ f Δ)
  (T : CType n m k) :
  TVarSubst (Γ.var T) f (Δ.var (T.trename 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 CVarSubst.ext {Γ : Context n m k}
  (σ : CVarSubst Γ f Δ)
  (T : CType n m k) :
  CVarSubst (Γ.var T) f (Δ.var (T.crename f)) :=

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 SSubtyp.dealias_right_forall.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType n m k)
  : Prop := True

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

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

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

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.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T2 E2} (ht : Γ.IsTight) (hd : SType.Dealias Γ S2 (SType.tforall T2 E2)),
    ∃ T1 E1, SType.Dealias Γ S1 (SType.tforall T1 E1)

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

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

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

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

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

def SSubtyp.dealias_tforall_inv.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T1 E1 T2 E2}
    (ht : Γ.IsTight)
    (h1 : SType.Dealias Γ S1 (SType.tforall T1 E1))
    (h2 : SType.Dealias Γ S2 (SType.tforall T2 E2)),
    SSubtyp Γ T2 T1 ∧ ESubtyp (Γ.tvar (TBinding.bound T2)) E1 E2

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

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

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

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

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

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.dealias_right_boxed.emotive
  (Γ : Context n m k)
  (E1 : EType n m k)
  (E2 : EType 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_right_boxed.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T2} (ht : Γ.IsTight) (hd : SType.Dealias Γ S2 (SType.box T2)),
    ∃ T1, SType.Dealias Γ S1 (SType.box T1)

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

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

def SSubtyp.dealias_boxed_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.box T1))
    (h2 : SType.Dealias Γ S2 (SType.box T2)),
    CSubtyp Γ T1 T2

def SSubtyp.dealias_right_label.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_label.smotive
  (Γ : Context n m k)
  (S1 : SType n m k)
  (S2 : SType n m k)
  : Prop :=
  ∀ {T2} (ht : Γ.IsTight) (hd : SType.Dealias Γ S2 (SType.label T2)),
    ∃ T1, SType.Dealias Γ S1 (SType.label T1)

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

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

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

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

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

def CType.open (C : CType (n+1) m k) (x : Fin n) : CType n m k :=
  C.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 EType.topen (E : EType n (m+1) k) (X : Fin m) : EType n m k :=
  E.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 SType.topen (S : SType n (m+1) k) (X : Fin m) : SType n m k :=
  S.trename (FinFun.open X)

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

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)

@[simp]
def EType.weaken_type :
  (EType.type T).weaken = EType.type (T.weaken) :=

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

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

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

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

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

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

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

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)

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)

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

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

inductive CType.IsValue : CType n m k -> Prop where
| capt :
  S.IsValue ->
  CType.IsValue (S^C)

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

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

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

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

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)

Nat in Init.Prelude

Fin in Init.Prelude

Fin.succ in Init.Data.Fin.Basic

Eq in Init.Prelude

Function.Injective in Init.Data.Function

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

EmptyCollection in Init.Core

Union in Init.Core

HasSubset in Init.Core

Exists in Init.Core

Or in Init.Prelude

Or.inr in Init.Prelude

And in Init.Prelude

Coe in Init.Coe

Fin.elim0 in Init.Data.Fin.Basic

Or.inl in Init.Prelude
</all_available_defs>

<all_available_lemmas>
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 Cont.HasLabel.tweaken
  (h : Cont.HasLabel cont x tail) :
  Cont.HasLabel cont.tweaken x tail.tweaken

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 IsValue.rename_l' {t : Term n m k} {t0 : Term n' m k}
  (he : t0 = t.rename f)
  (hv : t0.IsValue) :
  t.IsValue

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

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

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

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

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

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

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

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

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

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

theorem Term.crename_id {t : Term n m k} :
  t.crename FinFun.id = t

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 Term.crename_crename {t : Term n m k} {f : FinFun k k'} {g : FinFun k' k''} :
  (t.crename f).crename g = t.crename (g.comp f)

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

theorem Context.var_bound_succ_inv'
  (he1 : Γ0 = Γ.var P) (he1 : x0 = x.succ)
  (hb : Context.Bound Γ0 x0 T) :
  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken

theorem Context.var_bound_succ_inv
  (hb : Context.Bound (Γ.var P) x.succ T) :
  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken

theorem Context.var_tbound_inv'
  (he : Γ0 = Γ.var P)
  (hb : Context.TBound Γ0 X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.weaken

theorem Context.var_tbound_inv
  (hb : Context.TBound (Γ.var P) X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.weaken

theorem Context.var_tbound_inv_bound
  (hb : Context.TBound (Γ.var P) X (TBinding.bound S)) :
  ∃ S0, Context.TBound Γ X (TBinding.bound S0) ∧ S = SType.weaken S0

theorem Context.var_cbound_inv'
  (he : Γ0 = Γ.var P)
  (hb : Context.CBound Γ0 X b) :
  ∃ b0, Context.CBound Γ X b0 ∧ b = b0.weaken

theorem Context.var_cbound_inv
  (hb : Context.CBound (Γ.var P) X b) :
  ∃ b0, Context.CBound Γ X b0 ∧ b = b0.weaken

theorem Context.var_cbound_inv_bound
  (hb : Context.TBound (Γ.var P) X (TBinding.bound S)) :
  ∃ S0, Context.TBound Γ X (TBinding.bound S0) ∧ S = SType.weaken 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 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 Context.tbound_tbound_inst_inv'
  (he1 : Γ0 = Γ.tvar (TBinding.bound P))
  (he2 : b0 = TBinding.inst S)
  (hb : Context.TBound Γ0 X b0) :
  ∃ X0 S0, Context.TBound Γ X0 (TBinding.inst S0)
    ∧ S = SType.tweaken S0
    ∧ X = X0.succ

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.cvar_tbound_inv'
  (he : Γ0 = Γ.cvar p)
  (hb : Context.TBound Γ0 X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.cweaken

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

theorem Context.cvar_tbound_inv_bound
  (hb : Context.TBound (Γ.cvar p) X (TBinding.bound S)) :
  ∃ S0, Context.TBound Γ X (TBinding.bound S0) ∧ S = S0.cweaken

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.label_tbound_inv
  (hb : Context.TBound (Γ.label l) X b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.weaken

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 Context.tight_bound_tvar_absurd
  (ht : Context.IsTight Γ)
  (hb : Context.TBound Γ X (TBinding.bound S)) : False

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 Context.tvar_tbound_succ_inv
  (hb : Context.TBound (Γ.tvar p) (Fin.succ X) b) :
  ∃ b0, Context.TBound Γ X b0 ∧ b = b0.tweaken

theorem Context.cvar_tbound_tvar_inv'
  (he : Γ0 = Context.cvar Γ b)
  (hb : Context.TBound Γ0 X T) :
  ∃ T0, Context.TBound Γ X T0 ∧ T = T0.cweaken

theorem Context.cvar_tbound_tvar_inv
  (hb : Context.TBound (Context.cvar Γ b) X T) :
  ∃ T0, Context.TBound Γ X T0 ∧ T = T0.cweaken

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 Context.tvar_tbound_inv
  (hb : Context.TBound (Γ.tvar p) X b) :
  (X = 0 ∧ b = p.tweaken) ∨
  (∃ b0 X0, Context.TBound Γ X0 b0 ∧ b = b0.tweaken ∧ X = (Fin.succ X0))

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

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

theorem Context.cvar_cbound_inv'
  (he1 : Γ0 = Γ.cvar p)
  (hb : Context.CBound Γ0 X0 b) :
  (X0 = 0 ∧ b = p.cweaken) ∨
  (∃ b0 X, Context.CBound Γ X b0 ∧ b = b0.cweaken ∧ X0 = (Fin.succ X))

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

theorem Context.tbound_inj
  (h1 : Context.TBound Γ X b1)
  (h2 : Context.TBound Γ X b2) : b1 = b2

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

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

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

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

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

theorem Context.label_bound_succ_inv'
  (he1 : Γ0 = Γ.label l) (he2 : x0 = x.succ)
  (hb : Context.Bound Γ0 x0 T) :
  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken

theorem Context.label_bound_succ_inv
  (hb : Context.Bound (Γ.label l) x.succ T) :
  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken

theorem Context.cbound_injective
  (hb1 : Context.CBound Γ c b1)
  (hb2 : Context.CBound Γ c b2) : b1 = b2

theorem Context.bound_injective
  (hb1 : Context.Bound Γ x T1)
  (hb2 : Context.Bound Γ x T2) : T1 = T2

theorem Context.lbound_inj
  (hb1 : Context.LBound Γ x S1)
  (hb2 : Context.LBound Γ x S2) : S1 = S2

theorem Context.var_cbound_inv_inst'
  (he : b = CBinding.inst C)
  (hb : Context.CBound (Γ.var T) c b) :
  ∃ C0, Context.CBound Γ c (CBinding.inst C0) ∧ C = C0.weaken

theorem Context.var_cbound_inv_inst
  (hb : Context.CBound (Γ.var T) c (CBinding.inst C)) :
  ∃ C0, Context.CBound Γ c (CBinding.inst C0) ∧ C = C0.weaken

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 Context.cvar_bound_cbound_inv_inst
  (hb : Context.CBound (Γ,c<:B) c (CBinding.inst C)) :
  ∃ c0 C0, Context.CBound Γ c0 (CBinding.inst C0)
    ∧ c = c0.succ
    ∧ C = C0.cweaken

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

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

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

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

theorem ESubtyp.csubst
  (h : ESubtyp Γ E1 E2)
  (σ : CVarSubst Γ f Δ) :
  ESubtyp Δ (E1.crename f) (E2.crename f)

theorem CSubtyp.cinstantiate {Γ : Context n m k}
  (h : CSubtyp (Γ.cvar (CBinding.bound CBound.star)) T1 T2) :
  CSubtyp (Γ.cvar (CBinding.inst C)) T1 T2

theorem CaptureSet.rename_union {C1 C2 : CaptureSet n k} {f : FinFun n n'} :
  (C1 ∪ C2).rename f = C1.rename f ∪ C2.rename f

theorem CaptureSet.crename_union {C1 C2 : CaptureSet n k} {f : FinFun k k'} :
  (C1 ∪ C2).crename f = C1.crename f ∪ C2.crename f

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

theorem CaptureSet.rename_singleton {x : Fin n} {f : FinFun n n'} :
  ({x=x} : CaptureSet n k).rename f = {x=f x}

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

theorem CaptureSet.rename_csingleton {x : Fin k} {f : FinFun n n'} :
  {c=x}.rename f = {c=x}

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

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

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

theorem CaptureSet.crename_empty :
  ({} : CaptureSet n k).crename f = {}

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

theorem CaptureSet.copen_rename_comm {C : CaptureSet n (k+1)} {x : Fin k} {f : FinFun n n'} :
  (C.copen x).rename f = (C.rename f).copen x

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

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

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

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

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

theorem CaptureSet.crename_copen {C : CaptureSet n (k+1)} :
  (C.copen c).crename f = (C.crename f.ext).copen (f c)

theorem CaptureSet.cweaken_crename {C : CaptureSet n k} :
  (C.crename f).cweaken = C.cweaken.crename f.ext

theorem CaptureSet.subset_refl {C : CaptureSet n k} :
  C ⊆ C

theorem CaptureSet.cweaken_csingleton {c : Fin k} :
  (CaptureSet.csingleton c : CaptureSet n k).cweaken = CaptureSet.csingleton (c.succ)

theorem CaptureSet.weaken_csingleton :
  ({c=c} : CaptureSet n k).weaken = {c=c}

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

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

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

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

theorem CaptureSet.cweaken_def {C : CaptureSet n k} :
  C.cweaken = C.crename FinFun.weaken

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 SSubtyp.lweaken
  (h : SSubtyp Γ S1 S2) :
  ∀ S, SSubtyp (Γ.label S) S1.weaken S2.weaken

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

theorem CSubtyp.lweaken
  (h : CSubtyp Γ E1 E2) :
  CSubtyp (Γ.label S) E1.weaken E2.weaken

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

theorem ESubtyp.lweaken
  (h : ESubtyp Γ E1 E2) :
  ESubtyp (Γ.label S) 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 CBound.crename_rename_comm {b : CBound n k} :
  (b.crename f).rename g = (b.rename g).crename f

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

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

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

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

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

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

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 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 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 EType.cweaken_rename_comm {E : EType n m k} :
  E.cweaken.rename f = (E.rename f).cweaken

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

theorem SType.cweaken_rename_comm {S : SType n m k} :
  S.cweaken.rename f = (S.rename f).cweaken

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

theorem CType.copen_rename_comm {C : CType n m (k+1)} :
  (C.copen x).rename f = (C.rename f).copen 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 EType.weaken_rename {E : EType n m k} :
  (E.rename f).weaken = E.weaken.rename f.ext

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

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

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

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

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 EType.tweaken_rename {E : EType n m k} :
  E.tweaken.rename f = (E.rename f).tweaken

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

theorem SType.tweaken_rename {S : SType n m k} :
  S.tweaken.rename f = (S.rename f).tweaken

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

theorem EType.rename_copen :
  (EType.copen E c).rename f = (E.rename f).copen c

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

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

theorem EType.weaken_crename {E : EType n m k} :
  (E.crename f).weaken = E.weaken.crename f

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

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

theorem EType.tweaken_crename {E : EType n m k} :
  (E.crename f).tweaken = E.tweaken.crename f

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

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

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

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

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

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

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

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

theorem CType.weaken_trename {C : CType n m k} :
  (C.trename f).weaken = C.weaken.trename 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 CType.trename_trename (T : CType n m k) (f : FinFun m m') (g : FinFun m' m'') :
  (T.trename f).trename g = T.trename (g ∘ f)

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

theorem SType.cweaken_trename {S : SType n m k} :
  (S.trename f).cweaken = S.cweaken.trename f

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

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

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

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

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

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

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

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

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

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

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

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

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 EType.ex_cweaken_eq_inv {E : EType n m k}
  (heq : EType.ex (CType.capt C S) = E.cweaken) :
  ∃ C0 S0, E = EType.ex (CType.capt C0 S0) ∧ C0.cweaken1 = C ∧ S0.cweaken1 = S

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 EType.trename_id {E : EType n m k} :
  E.trename FinFun.id = E

theorem CType.trename_id {T : CType n m k} :
  T.trename FinFun.id = T

theorem SType.trename_id {S : SType n m k} :
  S.trename FinFun.id = S

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

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

theorem SType.crename_id {S : SType n m k} :
  S.crename FinFun.id = S

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

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

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

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

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

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

theorem CSubtyp.rename
  (h : CSubtyp Γ T1 T2)
  (ρ : VarMap Γ f Δ) :
  CSubtyp Δ (T1.rename f) (T2.rename f)

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

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

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

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

theorem FinFun.open_comp {f : FinFun n n'} {x : Fin n} :
  f ∘ FinFun.open x = FinFun.open (f x) ∘ f.ext

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

theorem FinFun.open_zero_comp_weaken_ext :
  (FinFun.open 0) ∘ (weaken.ext : FinFun (n+1) (n+2)) = id

theorem FinFun.id_ext :
  (FinFun.ext (n := n) id) = id

theorem FinFun.comp_succ {f : FinFun n n'}: Fin.succ ∘ f = (FinFun.ext f) ∘ Fin.succ

theorem FinFun.ext_zero {f : FinFun n n'} : f.ext 0 = 0

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

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

theorem Typed.weaken_ext {Γ : Context n m k}
  (h : Typed (Γ.var T) t E Ct) :
  Typed ((Γ.var P).var T.weaken) t.weaken1 E.weaken1 Ct.weaken1

theorem Typed.lweaken_ext {Γ : Context n m k}
  (h : Typed (Γ.var T) t E Ct) :
  Typed ((Γ.label P).var T.weaken) t.weaken1 E.weaken1 Ct.weaken1

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

theorem 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 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 Subbound.trename
  (h : Subbound Γ T1 T2)
  (ρ : TVarMap Γ f Δ) :
  Subbound Δ T1 T2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem TBinding.tweaken_rename_comm {b : TBinding n m k} :
  b.tweaken.rename f = (b.rename f).tweaken

theorem TBinding.weaken_crename {b : TBinding n m k} :
  (b.crename f).weaken = b.weaken.crename f

theorem CBinding.weaken_crename {b : CBinding n k} :
  (b.crename f).weaken = b.weaken.crename f

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

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

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

theorem TBinding.weaken_trename {b : TBinding n m k} :
  (b.trename f).weaken = b.weaken.trename f

theorem TBinding.cweaken_trename {b : TBinding n m k} :
  (b.trename f).cweaken = b.cweaken.trename f

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

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

theorem TBinding.trename_id {b : TBinding n m k} :
  b.trename FinFun.id = b

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

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

theorem Context.cvar_bound_var_inv'
  (he : Γ0 = Context.cvar Γ b)
  (hb : Context.Bound Γ0 x E) :
  ∃ E0, Context.Bound Γ x E0 ∧ E = E0.cweaken

theorem Context.cvar_bound_var_inv
  (hb : Context.Bound (Context.cvar Γ b) x E) :
  ∃ E0, Context.Bound Γ x E0 ∧ E = E0.cweaken

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

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

@[simp]
lemma TBinding.tweaken_bound: (TBinding.bound T).tweaken = TBinding.bound (T.tweaken)

@[simp]
lemma TBinding.tweaken_inst: (TBinding.inst T).tweaken = TBinding.inst (T.tweaken)

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

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

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

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

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

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

lemma TBinding.crename_bound: (TBinding.bound T).crename f = TBinding.bound (T.crename f)

lemma CBinding.crename_inst: (CBinding.inst T).crename f = CBinding.inst (T.crename f)

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

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

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

theorem ESubtyp.subst
  (h : ESubtyp Γ E1 E2)
  (σ : VarSubst Γ f Δ) :
  ESubtyp Δ (E1.rename f) (E2.rename f)

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

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

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

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

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

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

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

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

theorem Typed.precise_capture
  (h : Typed Γ (Term.var x) (EType.type (CType.capt C S)) C0) :
  Typed Γ (Term.var x) (EType.type (CType.capt {x=x} S)) {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.precise_cv
  (h : Typed Γ (Term.var x) E C0) :
  Typed Γ (Term.var x) E {x=x}

theorem SType.dealias_inj {S : SType n m k}
  (hd1 : SType.Dealias Γ S S1)
  (hd2 : SType.Dealias Γ S S2) :
  (S1.IsVar) ∨ (S2.IsVar) ∨ (S1 = S2)

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 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 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 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 Store.lookup_exists {σ : Store n m k} {x : Fin n} :
  (∃ v, Store.Bound σ x v ∧ v.IsValue) ∨ (∃ S, Store.LBound σ x S)

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 Store.value_typing_label_absurd'
  (hg : Γ.IsTight)
  (he : E0 = EType.type (S0^C))
  (hd : SType.Dealias Γ S0 (Label[S]))
  (ht : Typed Γ v E0 Cv)
  (hv : v.IsValue) : False

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

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

theorem progress
  (ht : TypedState state Γ E) :
  Progress state

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

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.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.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.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.var_inv'
  (he1 : t0 = Term.var x)
  (he2 : E0 = EType.type T)
  (h : Typed Γ t0 E0 Ct0) (hb : Γ.Bound x T0) :
  ∃ C0 S0, Γ.Bound x (S0^C0) ∧ (Γ ⊢ (S0^{x=x}) <: T)

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

theorem 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_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_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.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.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.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.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 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.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.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.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 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.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 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.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 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_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 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.forall_inv' {v : Term n m k}
  (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S0 (SType.forall T E))
  (he : E0 = EType.type (CType.capt Cv S0))
  (hv : v.IsValue)
  (ht : Typed Γ v E0 Ct) :
  ∃ T0 t, v = Term.lam T0 t

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 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 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 Typed.cforall_inv' {v : Term n m k}
  (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S0 (SType.cforall B E))
  (he : E0 = EType.type (CType.capt Cv S0))
  (hv : v.IsValue)
  (ht : Typed Γ v E0 Ct) :
  ∃ B0 t, v = Term.clam B0 t

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

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

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

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

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

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

theorem Typed.tapp_inv_capt
  (ht : Typed Γ (Term.tapp x X) 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.capp_inv_capt
  (ht : Typed Γ (Term.capp x c) E Ct) :
  Γ ⊢ ({x=x}) <:c Ct

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

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

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

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

theorem 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.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 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_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.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 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 WellScoped.subset
  (hsc : WellScoped Γ cont C)
  (hs : C' ⊆ C) :
  WellScoped Γ cont C'

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

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

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

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

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

theorem WellScoped.label_inv
  (hsc : WellScoped Γ cont {x=x})
  (hbl : Γ.LBound x S) :
  ∃ tail, cont.HasLabel x tail

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

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

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

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 CaptureSet.cweaken1_cweaken (C : CaptureSet n k) :
  C.cweaken.cweaken1 = C.cweaken.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 TypedCont.cweaken
  (h : TypedCont Γ E t E' Ct) :
  TypedCont (Γ.cvar b) E.cweaken t.cweaken E'.cweaken Ct.cweaken

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.copen
  (h : Typed (Γ,c<:CBound.upper {c=c}) t E Ct) :
  Typed Γ (t.copen c) (E.copen c) (Ct.copen c)

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

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

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.lookup_inv_typing_alt
  (hl : Store.Bound σ x v)
  (ht : TypedStore σ Γ)
  (hx : Typed Γ (Term.var x) (EType.type (S^C)) Cx) :
  ∃ C0 Cv0, Typed Γ v (EType.type (S^C0)) Cv0

theorem 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.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 Typed.topen
  (h : Typed (Γ,X<: (SType.tvar X)) t E Ct) :
  Typed Γ (t.topen X) (E.topen X) Ct

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

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

theorem SSubtyp.dealias_right_forall
  (h : SSubtyp Γ S1 S2) (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S2 (SType.forall T2 E2)) :
  ∃ T1 E1, SType.Dealias Γ S1 (SType.forall T1 E1)

theorem SSubtyp.dealias_right_tforall
  (h : SSubtyp Γ S1 S2) (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S2 (SType.tforall T2 E2)) :
  ∃ T1 E1, SType.Dealias Γ S1 (SType.tforall T1 E1)

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

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

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

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

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

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

theorem SSubtyp.dealias_right_cforall
  (h : SSubtyp Γ S1 S2) (ht : Γ.IsTight)
  (hd : SType.Dealias Γ S2 (SType.cforall B2 E2)) :
  ∃ B1 E1, SType.Dealias Γ S1 (SType.cforall B1 E1)

theorem SType.dealias_cforall_inj'
  (he1 : S1 = SType.cforall B1 E1) (he2 : S2 = SType.cforall B2 E2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  B1 = B2 ∧ E1 = E2

theorem SType.dealias_cforall_inj
  (h1 : SType.Dealias Γ S (SType.cforall B1 E1))
  (h2 : SType.Dealias Γ S (SType.cforall B2 E2)) :
  B1 = B2 ∧ E1 = E2

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

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

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 SType.dealias_boxed_inj
  (h1 : SType.Dealias Γ S (SType.box T1))
  (h2 : SType.Dealias Γ S (SType.box T2)) :
  T1 = T2

theorem SSubtyp.sub_dealias_boxed_inv
  (ht : Γ.IsTight)
  (h1 : SType.Dealias Γ S1 (SType.box T1))
  (h2 : SType.Dealias Γ S2 (SType.box T2))
  (hs : SSubtyp Γ S1 S2) :
  CSubtyp Γ T1 T2

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 SType.dealias_label_inj'
  (he1 : S1 = SType.label T1) (he2 : S2 = SType.label T2)
  (h1 : SType.Dealias Γ S S1)
  (h2 : SType.Dealias Γ S S2) :
  T1 = T2

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

theorem SSubtyp.sub_dealias_label_inv
  (ht : Γ.IsTight)
  (h1 : SType.Dealias Γ S1 (SType.label T1))
  (h2 : SType.Dealias Γ S2 (SType.label T2))
  (hs : SSubtyp Γ S1 S2) :
  SSubtyp Γ T2 T1

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

theorem ESubtyp.tnarrow
  (h : ESubtyp (Γ.tvar (TBinding.bound S)) E1 E2)
  (hs : SSubtyp Γ S' S) :
  ESubtyp (Γ.tvar (TBinding.bound S')) E1 E2

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

theorem Subcapt.refl :
  Subcapt Γ C C

theorem Subcapt.join
  (h1 : Γ ⊢ C1 <:c D1)
  (h2 : Γ ⊢ C2 <:c D2) :
  Γ ⊢ C1 ∪ C2 <:c D1 ∪ D2

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

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

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

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

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

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

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

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

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

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 Typed.narrow
  (h : Typed (Γ,x: T) t E Ct)
  (hs : CSubtyp Γ T' T) :
  Typed (Γ,x: T') t E Ct

theorem Typed.tnarrow
  (h : Typed (Γ,X<: S) t E Ct)
  (hs : SSubtyp Γ S' S) :
  Typed (Γ,X<: S') t E Ct

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

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

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

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

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 ESubtyp.type_inv_subcapt
  (h : ESubtyp Γ E (EType.type (CType.capt C S))) :
  ∃ C0 S0, E = EType.type (CType.capt C0 S0) ∧ Subcapt Γ C0 C

theorem ESubtyp.ex_inv_subcapt
  (h : ESubtyp Γ E (EType.ex (CType.capt C S))) :
  ∃ C0 S0, E = EType.ex (CType.capt C0 S0) ∧ Subcapt (Γ.cvar (CBinding.bound CBound.star)) C0 C

theorem CSubtyp.refl :
  CSubtyp Γ T T

theorem ESubtyp.refl :
  ESubtyp Γ E E

theorem CSubtyp.trans
  (h1 : CSubtyp Γ T1 T2)
  (h2 : CSubtyp Γ T2 T3) :
  CSubtyp Γ T1 T3

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

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)

@[simp]
theorem SType.rename_label :
  (SType.label S).rename f = SType.label (S.rename f)

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

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

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

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

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

theorem value_typing_widen
  (hv : Typed Γ v (EType.type (S^C)) Cv)
  (hs : Γ ⊢ (S^C1) <: (S'^C2)) :
  Typed Γ v (S'^C) Cv

theorem EType.weaken_cweaken_helper {S : SType n m k} :
  (EType.type (S^{})).weaken.cweaken = EType.type (S.weaken.cweaken^{})

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

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

theorem TypedStore.is_tight
  (h : TypedStore σ Γ) :
  Γ.IsTight
</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 TypedCont.lweaken
  (h : TypedCont Γ E cont E' Ct) :
  TypedCont (Γ.label S) E.weaken cont.weaken E'.weaken Ct.weaken :=
</target_theorem>

