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 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]
def CaptureSet.crename (C : CaptureSet n k) (f : FinFun k k') : CaptureSet n k' :=
  match C with
  | empty => empty
  | union C1 C2 => (C1.crename f) ∪ (C2.crename f)
  | singleton x => {x=x}
  | csingleton c => {c=f c}

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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)

infix:30 "

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

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

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

Function.Injective in Init.Data.Function

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

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

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

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

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)

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

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

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

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

def TVarSubst.text {Γ : Context n m k}
  (σ : TVarSubst Γ f Δ)
  (T : TBinding n m k) :
  TVarSubst (Γ.tvar T) f.ext (Δ.tvar (T.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)

instance : Coe (CType n m k) (EType n m k) where
  coe T := EType.type T

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 Subcapt.weaken
  (h : Γ ⊢ C1 <:c C2) :
  (Γ,x: T) ⊢ C1.weaken <:c C2.weaken :=

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

Or in Init.Prelude

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

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

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

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

@[aesop safe [constructors, cases]]

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

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

Coe in Init.Coe

@[simp]
def EType.tweaken_type :
  (EType.type T).tweaken = EType.type (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) :=

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

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

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

Fin.succ in Init.Data.Fin.Basic

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

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

def EType.cweaken (E : EType n m k) : EType n m (k+1) :=
  E.crename FinFun.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

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

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

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

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

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

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

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

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

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

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

Fin in Init.Prelude

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 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 VarSubst.open
  (hx : Typed Γ (Term.var x) (EType.type T) Cx) :
  VarSubst (Γ.var T) (FinFun.open x) Γ :=

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

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

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

<all_available_lemmas>
theorem Term.IsValue.cweaken
  (hv : Term.IsValue t) :
  Term.IsValue t.cweaken

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

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

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

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

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

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

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 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 CaptureSet.cweaken_csingleton {c : Fin k} :
  (CaptureSet.csingleton c : CaptureSet n k).cweaken = CaptureSet.csingleton (c.succ)

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

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

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

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

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

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

theorem SType.dealias_boxed_inj
  (h1 : SType.Dealias Γ S (SType.box T1))
  (h2 : SType.Dealias Γ S (SType.box T2)) :
  T1 = T2

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

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 Subbound.cweaken
  (h : Subbound Γ B1 B2) :
  Subbound (Γ.cvar b) B1.cweaken B2.cweaken

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

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

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

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

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

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

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

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

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

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 EType.weaken_cweaken_helper {S : SType n m k} :
  (EType.type (S^{})).weaken.cweaken = EType.type (S.weaken.cweaken^{})

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

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 CSubtyp.rename
  (h : CSubtyp Γ T1 T2)
  (ρ : VarMap Γ f Δ) :
  CSubtyp Δ (T1.rename f) (T2.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 CBinding.cweaken_bound :
  (CBinding.bound b : CBinding n k).cweaken = (CBinding.bound b.cweaken)

theorem CaptureSet.cweaken_rename_comm {C : CaptureSet n k} {f : FinFun n n'} :
  (C.cweaken).rename f = (C.rename f).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 Context.bound_lbound_absurd
  (hb1 : Context.Bound Γ x T)
  (hb2 : Context.LBound Γ x S) : False

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

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

theorem Typed.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 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 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 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 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 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 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.weaken_rename {S : SType n m k} :
  (S.rename f).weaken = S.weaken.rename f.ext

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

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

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

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)

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

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

theorem 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 ESubtyp.trename
  (h : ESubtyp Γ E1 E2)
  (ρ : TVarMap Γ f Δ) :
  ESubtyp Δ (E1.trename f) (E2.trename f)

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

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 CBinding.crename_rename_comm {b : CBinding n k} :
  (b.crename f).rename g = (b.rename g).crename f

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

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 CBinding.crename_id {b : CBinding n k} :
  b.crename FinFun.id = b

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 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 FinFun.open_zero_comp_weaken_ext :
  (FinFun.open 0) ∘ (weaken.ext : FinFun (n+1) (n+2)) = id

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

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 CaptureSet.weaken_crename {C : CaptureSet n k} :
  (C.crename f).weaken = C.weaken.crename f

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 Subbound.crename
  (h : Subbound Γ B1 B2)
  (ρ : CVarMap Γ f Δ) :
  Subbound Δ (B1.crename f) (B2.crename f)

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

theorem Subcapt.refl :
  Subcapt Γ C C

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 CSubtyp.lweaken
  (h : CSubtyp Γ E1 E2) :
  CSubtyp (Γ.label S) E1.weaken E2.weaken

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

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

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

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

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

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

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

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

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

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

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 SType.copen_rename_comm {S : SType n m (k+1)} :
  (S.copen x).rename f = (S.rename f).copen x

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

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

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

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

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

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

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

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

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 CSubtyp.cinstantiate {Γ : Context n m k}
  (h : CSubtyp (Γ.cvar (CBinding.bound CBound.star)) T1 T2) :
  CSubtyp (Γ.cvar (CBinding.inst C)) T1 T2

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 CaptureSet.weaken_csingleton :
  ({c=c} : CaptureSet n k).weaken = {c=c}

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

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

theorem ESubtyp.refl :
  ESubtyp Γ E E

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

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

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.var_inv_capt
  (hx : Typed Γ (Term.var x) E Cx) :
  Γ ⊢ ({x=x}) <:c Cx

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

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 SSubtyp.tweaken
  (h : SSubtyp Γ S1 S2) :
  SSubtyp (Γ.tvar b) S1.tweaken S2.tweaken

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

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 TBinding.trename_rename_comm {b : TBinding n m k} :
  (b.rename f).trename g = (b.trename g).rename f

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

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.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.tnarrow
  (h : Typed (Γ,X<: S) t E Ct)
  (hs : SSubtyp Γ S' S) :
  Typed (Γ,X<: S') t E Ct

theorem Store.lookup_exists {σ : Store n m k} {x : Fin n} :
  (∃ v, Store.Bound σ x v ∧ v.IsValue) ∨ (∃ S, Store.LBound σ x S)

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

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

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

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 Subcapt.trename
  (h : Subcapt Γ C1 C2)
  (ρ : TVarMap Γ f Δ) :
  Subcapt Δ C1 C2

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

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 CaptureSet.Subset.crename {C1 C2 : CaptureSet n k}
  (h : C1 ⊆ C2) :
  C1.crename f ⊆ C2.crename f

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

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

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

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

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

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

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

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

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

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

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 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 TBinding.weaken_trename {b : TBinding n m k} :
  (b.trename f).weaken = b.weaken.trename f

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

theorem CBinding.rename_id {b : CBinding n k} :
  b.rename FinFun.id = b
</all_available_lemmas>

<local_ctx>
import Capless.Type.Core

import Capless.Type.Renaming

namespace Capless

end

end

end

end
</local_ctx>

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

