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 Par : Term → Term → Prop where
  | β {b b' a a' c} :
    b ⇒ b' →
    a ⇒ a' →
    
    app (abs c b) a ⇒ subst (a' +: var) b'
  | var s : var s ⇒ var s
  | 𝒰 {a a'} :
    a ⇒ a' →
    
    𝒰 a ⇒ 𝒰 a'
  | pi {a a' b b'} :
    a ⇒ a' →
    b ⇒ b' →
    
    pi a b ⇒ pi a' b'
  | abs {a a' b b'} :
    a ⇒ a' →
    b ⇒ b' →
    
    abs a b ⇒ abs a' b'
  | app {b b' a a'} :
    b ⇒ b' →
    a ⇒ a' →
    
    app b a ⇒ app b' a'
  | mty : mty ⇒ mty
  | exf {a a' b b'} :
    a ⇒ a' →
    b ⇒ b' →
    
    exf a b ⇒ exf a' b'
  | lvl {a a'} :
    a ⇒ a' →
    
    lvl a ⇒ lvl a'
  | lof k : lof k ⇒ lof k

inductive Pars : Term → Term → Prop where
  | refl a : a ⇒⋆ a
  | trans {a b c} : a ⇒ b → b ⇒⋆ c → a ⇒⋆ c

@[simp]
def taka : Term → Term
  | 𝒰 a => 𝒰 (taka a)
  | pi a b => pi (taka a) (taka b)
  | abs a b => abs (taka a) (taka b)
  | app b a => match b with
    | abs _ b => subst (taka a +: var) (taka b)
    | b => app (taka b) (taka a)
  | exf a b => exf (taka a) (taka b)
  | lvl a => lvl (taka a)
  | t => t

def Conv (a : Term) (b : Term) : Prop := ∃ c, a ⇒⋆ c ∧ b ⇒⋆ c

inductive Interp (i : lc.L) (I : ∀ j, j < i → Term → Prop) : Term → (Term → Prop) → Prop where
  | ne a : ne a → Interp i I a wne
  | pi a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp i I a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp i I (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 j (lt : j < i) : Interp i I (𝒰 (lof j)) (I j lt)
  | mty : Interp i I mty wne
  | lvl b : nf b → Interp i I (lvl b)
    (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)
  | step a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j _ a ↦ ∃ P, Interps j a P)
termination_by i

@[simp]
def CR (P : Term → Prop) : Prop :=
  ∀ a, (wne a → P a) ∧ (P a → wnf a)

def semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

@[simp]
def idType k := (pi (lvl (lof k)) (pi (𝒰 (var 0)) (pi (var 0) (var 1))))

def main : IO Unit :=
  pure ()

inductive Interp (i : lc.L) (I : lc.L → Term → Prop) : Term → (Term → Prop) → Prop where
  | ne a : ne a → Interp i I a wne
  | pi a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp i I a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp i I (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 b : wnf b → Interp i I (𝒰 b)
    (λ a ↦ (∃ j, b ⇒⋆ lof j ∧ I j a) ∨ wne a)
  | mty : Interp i I mty wne
  | lvl b : wnf b → Interp i I (lvl b)
    (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)
  | step a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j a ↦ if j < i then (∃ P, Interps j a P) else False)
termination_by i

@[simp]
def CR (P : Term → Prop) : Prop :=
  ∀ a, (wne a → P a) ∧ (P a → wnf a)

def semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

@[simp]
def cons {A : Type} (x : A) (ξ : Nat → A) : Nat → A
  | 0 => x
  | n + 1 => ξ n

inductive Term : Type where
  | var : Nat → Term
  | 𝒰 : Term → Term
  | pi : Term → Term → Term
  | abs : Term → Term → Term
  | app : Term → Term → Term
  | mty : Term
  | exf : Term → Term → Term
  | lvl : Term → Term
  | lof : lc.L → Term

@[simp]
def lift (ξ : Nat → Nat) : Nat → Nat :=
  zero +: (succ ∘ ξ)

@[simp]
def rename (ξ : Nat → Nat) : Term → Term
  | var s => var (ξ s)
  | 𝒰 a => 𝒰 (rename ξ a)
  | pi a b => pi (rename ξ a) (rename (lift ξ) b)
  | abs a b => abs (rename ξ a) (rename (lift ξ) b)
  | app b a => app (rename ξ b) (rename ξ a)
  | mty => mty
  | exf a b => exf (rename ξ a) (rename ξ b)
  | lvl a => lvl (rename ξ a)
  | lof k => lof k

@[simp]
def up (σ : Nat → Term) : Nat → Term :=
  var 0 +: (rename succ ∘ σ)

@[simp]
def subst (σ : Nat → Term) : Term → Term
  | var s => σ s
  | 𝒰 a => 𝒰 (subst σ a)
  | pi a b => pi (subst σ a) (subst (⇑ σ) b)
  | abs a b => abs (subst σ a) (subst (⇑ σ) b)
  | app b a => app (subst σ b) (subst σ a)
  | mty => mty
  | exf a b => exf (subst σ a) (subst σ b)
  | lvl a => lvl (subst σ a)
  | lof k => lof k

def substId : ∀ s, subst var s = s :=
  substId' var (by admit /- proof elided -/
  )

def substRename ξ σ : ∀ s, subst σ (rename ξ s) = subst (σ ∘ ξ) s :=
  substRename' _ _ (σ ∘ ξ) (by admit /- proof elided -/
  )

def renameSubst ξ σ : ∀ s, rename ξ (subst σ s) = subst (rename ξ ∘ σ) s :=
  renameSubst' _ _ (rename ξ ∘ σ) (by admit /- proof elided -/
  )

def substComp σ τ : ∀ s, (subst σ ∘ subst τ) s = subst (subst σ ∘ τ) s :=
  substComp' _ _ (subst σ ∘ τ) (by admit /- proof elided -/
  )

inductive Ctxt : Type where
  | nil : Ctxt
  | cons : Ctxt → Term → Ctxt

inductive In : Nat → Term → Ctxt → Prop where
  | here {Γ A} : In 0 (rename succ A) (Γ ∷ A)
  | there {Γ x A B} : In x A Γ → In (succ x) (rename succ A) (Γ ∷ B)

def wRename ξ Γ Δ := ∀ x A, Γ ∋ x ∶ A → Δ ∋ ξ x ∶ rename ξ A

@[simp]
def nf : Term → Prop
  | 𝒰 a => nf a
  | pi a b => nf a ∧ nf b
  | abs a b => nf a ∧ nf b
  | app b a => ne b ∧ nf a
  | exf a b => nf a ∧ ne b
  | lvl a => nf a
  | _ => True

@[simp]
def ne : Term → Prop
  | var _ => True
  | app b a => ne b ∧ nf a
  | exf a b => nf a ∧ ne b
  | _ => False

@[simp] def wnf (a : Term) : Prop := ∃ b, nf b ∧ a ⇒⋆ b

@[simp] def wne (a : Term) : Prop := ∃ b, ne b ∧ a ⇒⋆ b

inductive Interp (i : lc.L) (I : ∀ j, j < i → Term → Prop) : Term → (Term → Prop) → Prop where
  | ne a : ne a → Interp i I a wne
  | pi a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp i I a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp i I (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 b : wnf b → Interp i I (𝒰 b)
    (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a)
  | mty : Interp i I mty wne
  | lvl b : wnf b → Interp i I (lvl b)
    (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)
  | step a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j _ a ↦ ∃ P, Interps j a P)
termination_by i

@[simp]
def CR (P : Term → Prop) : Prop :=
  ∀ a, (wne a → P a) ∧ (P a → wnf a)

def semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

inductive Interp : ∀ (i : lc.L), (∀ j, j < i → Term → Prop) → Term → (Term → Prop) → Prop where
  | ne i I a : ne a → Interp i I a wne
  | pi i I j le a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp j (λ k lt ↦ I k (transl lt le)) a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp j (λ k lt ↦ I k (transl lt le)) (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 i I b : wnf b → Interp i I (𝒰 b)
    (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a)
  | mty i I : Interp i I mty wne
  | lvl i I b : wnf b → Interp i I (lvl b)
    (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)
  | step i I a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j _ a ↦ ∃ P, Interps j a P)
termination_by i

@[simp]
def CR (P : Term → Prop) : Prop :=
  ∀ a, (wne a → P a) ∧ (P a → wnf a)

def semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

inductive Eqv : Term → Term → Prop where
  | β {b a c} : app (abs c b) a ≈ subst (a +: var) b
  | 𝒰 {a a'} :
    a ≈ a' →
    
    𝒰 a ≈ 𝒰 a'
  | pi {a a' b b'} :
    a ≈ a' →
    b ≈ b' →
    
    pi a b ≈ pi a' b'
  | abs {a a' b b'} :
    a ≈ a' →
    b ≈ b' →
    
    abs a b ≈ abs a' b'
  | app {b b' a a'} :
    b ≈ b' →
    a ≈ a' →
    
    app b a ≈ app b' a'
  | exf {a a' b b'} :
    a ≈ a' →
    b ≈ b' →
    
    exf a b ≈ exf a' b'
  | lvl {a a'} :
    a ≈ a' →
    
    lvl a ≈ lvl a'
  | refl {a} : a ≈ a
  | sym {a b} :
    a ≈ b →
    
    b ≈ a
  | trans {a b c} :
    a ≈ b →
    b ≈ c →
    
    a ≈ c

inductive Wf : Ctxt → Prop where
  | nil : ⊢ ⬝
  | cons {Γ A k} :
    ⊢ Γ →
    Γ ⊢ A ∶ 𝒰 k →
    
    ⊢ Γ ∷ A

inductive Wt : Ctxt → Term → Term → Prop where
  | var {Γ x A} :
    ⊢ Γ →
    Γ ∋ x ∶ A →
    
    Γ ⊢ var x ∶ A
  | 𝒰 {Γ j k} :
    Γ ⊢ j ∶ lvl k →
    
    Γ ⊢ 𝒰 j ∶ 𝒰 k
  | pi {Γ A B k} :
    Γ ⊢ A ∶ 𝒰 k →
    Γ ∷ A ⊢ B ∶ 𝒰 (rename succ k) →
    
    Γ ⊢ pi A B ∶ 𝒰 k
  | abs {Γ A B b k} :
    Γ ⊢ pi A B ∶ 𝒰 k →
    Γ ⊢ A ∶ 𝒰 k →
    Γ ∷ A ⊢ b ∶ B →
    
    Γ ⊢ abs A b ∶ pi A B
  | app {Γ A B b a} :
    Γ ⊢ b ∶ pi A B →
    Γ ⊢ a ∶ A →
    
    Γ ⊢ app b a ∶ subst (a +: var) B
  | mty {Γ j k} :
    Γ ⊢ 𝒰 j ∶ 𝒰 k →
    
    Γ ⊢ mty ∶ 𝒰 j
  | exf {Γ A b k} :
    Γ ⊢ A ∶ 𝒰 k →
    Γ ⊢ b ∶ mty →
    
    Γ ⊢ exf A b ∶ A
  | lvl {Γ a b j k} :
    Γ ⊢ a ∶ lvl b →
    Γ ⊢ 𝒰 j ∶ 𝒰 k →
    
    Γ ⊢ lvl a ∶ 𝒰 j
  | lof {Γ j k} :
    ⊢ Γ →
    j < k →
    
    Γ ⊢ lof j ∶ lvl (lof k)
  | trans {Γ i j k} :
    Γ ⊢ i ∶ lvl j →
    Γ ⊢ j ∶ lvl k →
    
    Γ ⊢ i ∶ lvl k
  | conv {Γ A B a k} :
    A ≈ B →
    Γ ⊢ a ∶ A →
    Γ ⊢ B ∶ 𝒰 k →
    
    Γ ⊢ a ∶ B
  | sub {Γ j k A} :
    Γ ⊢ j ∶ lvl k →
    Γ ⊢ A ∶ 𝒰 j →
    
    Γ ⊢ A ∶ 𝒰 k

@[induction_eliminator]
def wtInd {motive} :=
  @Wt.rec _ (λ _ _ ↦ True) motive (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  )

def firstArgEq? : Lean.Expr → Bool
  | .forallE _ bType _ .default =>
    Lean.Expr.isEq bType
  | .forallE _ _ body _ =>
    firstArgEq? body
  | _ => false

inductive Interp (i : lc.L) (I : ∀ j, j < i → Term → Prop) : Term → (Term → Prop) → Prop where
  | ne a : ne a → Interp i I a wne
  | pi a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp i I a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp i I (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 j (lt : j < i) : Interp i I (𝒰 (lof j)) (I j lt)
  | 𝒰ne a : ne a → Interp i I (𝒰 a) wne
  | mty : Interp i I mty wne
  | lvl b : nf b → Interp i I (lvl b)
    (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)
  | step a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j _ a ↦ ∃ P, Interps j a P)
termination_by i

@[simp]
def CR (P : Term → Prop) : Prop :=
  ∀ a, (wne a → P a) ∧ (P a → wnf a)

def semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

class LevelClasses (L : Type)
  extends Preorder L, OrderBot L, IsWellOrder L lt, NoMaxOrder L

instance {L : Type} [lc : LevelClasses L] : WellFoundedRelation L :=
  lc.toWellFoundedRelation

class LevelClass where
  L : Type
  lc : LevelClasses L

instance instNoMaxOrderNat : NoMaxOrder Nat where
  exists_gt := λ i ↦ ⟨Nat.succ i, by admit /- proof elided -/
  ⟩

@[simp]
instance : LevelClass where
  L := Nat
  lc := { bot := 0, bot_le := λ _ ↦ by simp }

inductive Interp (i : lc.L) (I : ∀ j, j < i → Term → Prop) : Term → (Term → Prop) → Prop where
  | pi a b Pa (Pf : Term → (Term → Prop) → Prop) :
    Interp i I a Pa →
    (∀ x, Pa x → ∃ Pb, Pf x Pb) →
    (∀ x Pb, Pf x Pb → Interp i I (subst (x +: var) b) Pb) →
    Interp i I (pi a b) (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))
  | 𝒰 j (lt : j < i) : Interp i I (𝒰 (lof j)) (I j lt)
  | mty : Interp i I mty (λ _ ↦ False)
  | lvl k : Interp i I (lvl (lof k)) (λ a ↦ ∃ j, a ⇒⋆ lof j ∧ j < k)
  | step a b P :
    a ⇒ b →
    Interp i I b P →
    Interp i I a P

def Interps (i : lc.L) : Term → (Term → Prop) → Prop :=
  Interp i (λ j _ a ↦ ∃ P, Interps j a P)
termination_by i

def semSubst σ Γ := ∀ x a, In x a Γ → ∃ i P, (⟦ subst σ a ⟧ i ↘ P) ∧ P (σ x)

def semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

def wSubst σ Γ Δ := ∀ x A, Γ ∋ x ∶ A → Δ ⊢ σ x ∶ subst σ A

inductive Value : Term → Type where
  | 𝒰 {k} : Value (𝒰 k)
  | pi {a b} : Value (pi a b)
  | abs {a b} : Value (abs a b)
  | mty : Value mty
  | lvl {k} : Value (lvl k)
  | lof {k} : Value (lof k)

inductive CBN : Term → Term → Prop where
  | β {b a c} : app (abs c b) a ⇒β subst (a +: var) b
  | app {b b' a} : b ⇒β  b' → app b a ⇒β app b' a
  | exf {a b b'} : b ⇒β b' → exf a b ⇒β exf a b'

inductive CBNs : Term → Term → Prop where
  | refl a : a ⇒β⋆ a
  | trans {a b c} : a ⇒β b → b ⇒β⋆ c → a ⇒β⋆ c

@[simp] 
def valueType {a} (A : Term) : Value a → Prop
  | Value.𝒰 | Value.pi | Value.mty | Value.lvl => ∃ k, 𝒰 k ≈ A
  | Value.abs => ∃ B C, pi B C ≈ A
  | Value.lof => ∃ k, lvl k ≈ A

IO in Init.System.IO

Unit in Init.Prelude

Nat.succ in Init.Prelude

IsTrans in Mathlib.Order.Defs.Unbundled

Nat.sub in Init.Prelude

Nonempty in Init.Prelude

Or in Init.Prelude

Or.inr in Init.Prelude

propext in Init.Core

Bool in Init.Prelude

Lean.Expr in Lean.Expr

Lean.Expr.isEq in Lean.Util.Recognizers

Or.inl in Init.Prelude

id in Init.Prelude

Nat in Init.Prelude

IsWellOrder in Mathlib.Order.RelClasses

NoMaxOrder in Mathlib.Order.Max

OrderBot in Mathlib.Order.BoundedOrder.Basic

Preorder in Mathlib.Order.Defs.PartialOrder

WellFoundedRelation in Init.WF

L in Archive.Hairer

Nat.zero in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem parRefl a : a ⇒ a

theorem parRename {a b} ξ (r : a ⇒ b) : rename ξ a ⇒ rename ξ b

theorem parLift σ τ (h : ∀ x, σ x ⇒ τ x) : ∀ x, (⇑ σ) x ⇒ (⇑ τ) x

theorem parMorphing {a b} σ τ (h : ∀ x, σ x ⇒ τ x) (r : a ⇒ b) : subst σ a ⇒ subst τ b

theorem parSubst {a b} σ (r : a ⇒ b) : subst σ a ⇒ subst σ b

theorem parCong {a a' b b'} (ra : a ⇒ a') (rb : b ⇒ b') : subst (a +: var) b ⇒ subst (a' +: var) b'

theorem antirenaming {ξ a b'} (r : rename ξ a ⇒ b') : ∃ b, b' = rename ξ b ∧ a ⇒ b

theorem parPars {a b} (r : a ⇒ b) : a ⇒⋆ b

theorem parsTrans {a b c} (r₁ : a ⇒⋆ b) (r₂ : b ⇒⋆ c) : a ⇒⋆ c

theorem parsRename {a b} ξ (r : a ⇒⋆ b) : rename ξ a ⇒⋆ rename ξ b

theorem parsSubst {a b} σ (r : a ⇒⋆ b) : subst σ a ⇒⋆ subst σ b

theorem parsCong {a a' b b'} (ra : a ⇒⋆ a') (rb : b ⇒⋆ b') : subst (a +: var) b ⇒⋆ subst (a' +: var) b'

theorem parsAntirenaming {ξ a b'} (r : rename ξ a ⇒⋆ b') : ∃ b, b' = rename ξ b ∧ a ⇒⋆ b

theorem pars𝒰 {a a'} (r : a ⇒⋆ a') : 𝒰 a ⇒⋆ 𝒰 a'

theorem parsPi {a a' b b'} (ra : a ⇒⋆ a') (rb : b ⇒⋆ b') : pi a b ⇒⋆ pi a' b'

theorem parsAbs {a a' b b'} (ra : a ⇒⋆ a') (rb : b ⇒⋆ b') : abs a b ⇒⋆ abs a' b'

theorem parsApp {a a' b b'} (rb : b ⇒⋆ b') (ra : a ⇒⋆ a') : app b a ⇒⋆ app b' a'

theorem parsExf {a a' b b'} (ra : a ⇒⋆ a') (rb : b ⇒⋆ b') : exf a b ⇒⋆ exf a' b'

theorem parsLvl {a a'} (r : a ⇒⋆ a') : lvl a ⇒⋆ lvl a'

theorem parsβ {b a c} σ : app (abs c (subst (⇑ σ) b)) a ⇒⋆ subst (a +: σ) b

theorem pars𝒰Inv {a b} (r : 𝒰 a ⇒⋆ b) : ∃ a', b = 𝒰 a' ∧ a ⇒⋆ a'

theorem parsMtyInv {b} (r : mty ⇒⋆ b) : b = mty

theorem parsPiInv {a b c} (r : pi a b ⇒⋆ c) : ∃ a' b', c = pi a' b' ∧ a ⇒⋆ a' ∧ b ⇒⋆ b'

theorem parsAbsInv {a b c} (r : abs a b ⇒⋆ c) : ∃ a' b', c = abs a' b' ∧ a ⇒⋆ a' ∧ b ⇒⋆ b'

theorem parsExfInv {a b c} (r : exf a b ⇒⋆ c) : ∃ a' b', c = exf a' b' ∧ a ⇒⋆ a' ∧ b ⇒⋆ b'

theorem parsLvlInv {i b} (r : lvl i ⇒⋆ b) : ∃ j, b = lvl j ∧ i ⇒⋆ j

theorem parsLofInv {j b} (r : lof j ⇒⋆ b) : b = lof j

theorem parTaka {a b} (r : a ⇒ b) : b ⇒ taka a

theorem diamond {a b c} (r₁ : a ⇒ b) (r₂ : a ⇒ c) : ∃ d, b ⇒ d ∧ c ⇒ d

theorem diacon {a b c} (r₁ : a ⇒⋆ b) (r₂ : a ⇒ c) : ∃ d, b ⇒⋆ d ∧ c ⇒⋆ d

theorem confluence {a b c} (r₁ : a ⇒⋆ b) (r₂ : a ⇒⋆ c) : ∃ d, b ⇒⋆ d ∧ c ⇒⋆ d

theorem parsConv {a b} (r : a ⇒⋆ b) : a ⇔ b

theorem parConv {a b} (r : a ⇒ b) : a ⇔ b

theorem convRefl {a} : a ⇔ a

theorem convSym {a b} : a ⇔ b → b ⇔ a

theorem convTrans {a b c} : a ⇔ b → b ⇔ c → a ⇔ c

theorem convRename {a b} ξ : a ⇔ b → rename ξ a ⇔ rename ξ b

theorem convSubst {a b} σ : a ⇔ b → subst σ a ⇔ subst σ b

theorem convCong {a a' b b'} : a ⇔ a' → b ⇔ b' → subst (a +: var) b ⇔ subst (a' +: var) b'

theorem conv𝒰 {a a'} : a ⇔ a' → 𝒰 a ⇔ 𝒰 a'

theorem convPi {a a' b b'} : a ⇔ a' → b ⇔ b' → pi a b ⇔ pi a' b'

theorem convAbs {a a' b b'} : a ⇔ a' → b ⇔ b' → abs a b ⇔ abs a' b'

theorem convApp {b b' a a'} : b ⇔ b' → a ⇔ a' → app b a ⇔ app b' a'

theorem convExf {a a' b b'} : a ⇔ a' → b ⇔ b' → exf a b ⇔ exf a' b'

theorem convLvl {a a'} : a ⇔ a' → lvl a ⇔ lvl a'

theorem conv𝒰Mty {a} : ¬ 𝒰 a ⇔ mty

theorem conv𝒰Pi {c a b} : ¬ 𝒰 c ⇔ pi a b

theorem convMtyPi {a b} : ¬ mty ⇔ pi a b

theorem convLvlPi {a b k} : ¬ lvl k ⇔ pi a b

theorem convLvl𝒰 {j k} : ¬ lvl j ⇔ 𝒰 k

theorem convLvlMty {j} : ¬ lvl j ⇔ mty

theorem convLvlInv {j k} : lvl j ⇔ lvl k → j ⇔ k

theorem conv𝒰Inv {a b} : 𝒰 a ⇔ 𝒰 b → a ⇔ b

theorem convPiInv {a₁ a₂ b₁ b₂} : pi a₁ b₁ ⇔ pi a₂ b₂ → a₁ ⇔ a₂ ∧ b₁ ⇔ b₂

theorem interpLvlEq {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a) =
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ c ⇒⋆ lof k) ∨ wne a)

theorem interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ i, I ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I a P} (h : ⟦ 𝒰 a ⟧ i , I ↘ P) :
  ∃ j lt, a ⇒⋆ lof j ∧ P = I j lt

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

theorem interpLvlInv {i I b P} (h : ⟦ lvl b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpsNe {i a} (nea : ne a) : ⟦ a ⟧ i ↘ wne

theorem interpsPi {i a b Pa P}
  (ha : ⟦ a ⟧ i ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i j} (lt : j < i) :
  ⟦ 𝒰 (lof j) ⟧ i ↘ (λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ wne

theorem interpsLvl {i b} (nfb : nf b) :
  ⟦ lvl b ⟧ i ↘ (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpDet' {i I a P Q} (hP : ⟦ a ⟧ i , I ↘ P) (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) : ⟦ a ⟧ j ↘ P

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i a P} (h : ⟦ 𝒰 a ⟧ i ↘ P) :
  ∃ j, j < i ∧ a ⇒⋆ lof j ∧ P = λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

theorem interpsLvlInv {i b P} (h : ⟦ lvl b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpWnf {i I a P}
  (adq : ∀ {a P}, (⟦ a ⟧ i , I ↘ P) → CR P)
  (h : ⟦ a ⟧ i , I ↘ P) : wnf a

theorem adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

theorem interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

theorem wfMty : ⊢ ⬝ ∷ mty

theorem wtfMty : ⬝ ∷ mty ⊢ var 0 ∶ mty

theorem loopLvl : ⬝ ∷ mty ⊢ exf (var 0) ∶ lvl (exf (var 0))

theorem loop : ⬝ ⊢ abs (𝒰 (exf (var 0))) ∶ pi mty (𝒰 (exf (var 0)))

theorem idpoly : ⬝ ⊢ (abs (abs (abs (var 0)))) ∶ idType 69

theorem idid : ⬝ ⊢ (abs (app (app ((app (var 0) (lof 3))) (idType 3)) (abs (app (var 1) (var 0))))) ∶ (pi (idType 4) (idType 3))

theorem semComp {ξ : ℕ → ℕ} {σ Γ Δ}
  (h : Δ ⊢ ξ ∶ Γ)
  (hζ : σ ⊨ Δ) :
  σ ∘ ξ ⊨ Γ

theorem semRename {ξ : ℕ → ℕ} {Γ Δ a A}
  (hξ : Δ ⊢ ξ ∶ Γ)
  (ha : Γ ⊨ a ∶ A) :
  Δ ⊨ rename ξ a ∶ rename ξ A

theorem semWeaken {Γ a A B}
  (ha : Γ ⊨ a ∶ A) :
  Γ ∷ B ⊨ rename succ a ∶ rename succ A

theorem semWfCons {Γ A k} (hΓ : ⊨ Γ) (hA : Γ ⊨ A ∶ 𝒰 k) : ⊨ Γ ∷ A

theorem soundness {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : Γ ⊨ a ∶ A

theorem normalization {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : wnf a ∧ wnf A

theorem what {i} : (λ j a ↦ if j < i then (∃ P, Interps j a P) else False) = (λ j a ↦ ∃ P, ⟦ a ⟧ j ↘ P)

theorem unfoldInterps {a i P} :
  (⟦ a ⟧ i ↘ P) =
  (⟦ a ⟧ i , (λ j b ↦ ∃ P, ⟦ b ⟧ j ↘ P) ↘ P)

theorem interp𝒰Eq {I : lc.L → Term → Prop} {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j, b ⇒⋆ lof j ∧ I j a) ∨ wne a) =
  (λ a ↦ (∃ j, c ⇒⋆ lof j ∧ I j a) ∨ wne a)

theorem interpLvlEq {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a) =
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ c ⇒⋆ lof k) ∨ wne a)

theorem interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ i, I ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I b P} (h : ⟦ 𝒰 b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j, b ⇒⋆ lof j ∧ I j a) ∨ wne a)

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

theorem interpLvlInv {i I b P} (h : ⟦ lvl b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpsNe {i a} (nea : ne a) : ⟦ a ⟧ i ↘ wne

theorem interpsPi {i a b Pa P}
  (ha : ⟦ a ⟧ i ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i b} (wnfb : wnf b) :
  ⟦ 𝒰 b ⟧ i ↘ (λ a ↦ (∃ j, b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ wne

theorem interpsLvl {i b} (wnfb : wnf b) :
  ⟦ lvl b ⟧ i ↘ (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpDet' {i I a P Q} (hP : ⟦ a ⟧ i , I ↘ P) (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) : ⟦ a ⟧ j ↘ P

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i b P} (h : ⟦ 𝒰 b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j, b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

theorem interpsLvlInv {i b P} (h : ⟦ lvl b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpWnf {i I a P}
  (adq : ∀ {a P}, (⟦ a ⟧ i , I ↘ P) → CR P)
  (h : ⟦ a ⟧ i , I ↘ P) : wnf a

theorem adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

theorem interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

omit lc in
theorem liftExt ξ ζ (h : ∀ x, ξ x = ζ x) : ∀ x, lift ξ x = lift ζ x

omit lc in
theorem liftId ξ (h : ∀ x, ξ x = x) : ∀ x, lift ξ x = x

omit lc in
theorem liftComp ξ ζ ς (h : ∀ x, (ξ ∘ ζ) x = ς x) :
  ∀ x, (lift ξ ∘ lift ζ) x = lift ς x

omit lc in
theorem liftSucc ξ : ∀ x, (lift ξ ∘ succ) x = (succ ∘ ξ) x

theorem renameExt ξ ζ (h : ∀ x, ξ x = ζ x) : ∀ s, rename ξ s = rename ζ s

theorem renameId s : rename id s = s

theorem renameComp' ξ ζ ς (h : ∀ x, (ξ ∘ ζ) x = ς x) : ∀ s, (rename ξ ∘ rename ζ) s = rename ς s

theorem renameComp ξ ζ s : rename ξ (rename ζ s) = rename (ξ ∘ ζ) s

theorem upUp σ x : (⇑ ⇑ σ) x = (var 0 +: var 1 +: (rename succ ∘ rename succ ∘ σ)) x

theorem upId σ (h : ∀ x, σ x = var x) : ∀ x, (⇑ σ) x = var x

theorem upExt σ τ (h : ∀ x, σ x = τ x) : ∀ x, (⇑ σ) x = (⇑ τ) x

theorem upLift ξ σ τ (h : ∀ x, (σ ∘ ξ) x = τ x) : ∀ x, (⇑ σ ∘ lift ξ) x = (⇑ τ) x

theorem upSucc σ : ∀ x, (⇑ σ ∘ succ) x = (rename succ ∘ σ) x

theorem upVar ξ : ∀ x, (var ∘ lift ξ) x = (⇑ (var ∘ ξ)) x

theorem upRename ξ σ τ (h : ∀ x, (rename ξ ∘ σ) x = τ x) : ∀ x, (rename (lift ξ) ∘ ⇑ σ) x = (⇑ τ) x

theorem substExt σ τ (h : ∀ x, σ x = τ x) : ∀ s, subst σ s = subst τ s

theorem substId' σ (h : ∀ x, σ x = var x) : ∀ s, subst σ s = s

theorem substRename' ξ σ τ (h : ∀ x, (σ ∘ ξ) x = τ x) : ∀ s, subst σ (rename ξ s) = subst τ s

theorem renameSubst' ξ σ τ (h : ∀ x, (rename ξ ∘ σ) x = τ x) : ∀ s, rename ξ (subst σ s) = subst τ s

theorem upSubst ρ σ τ (h : ∀ x, (subst ρ ∘ σ) x = τ x) : ∀ x, (subst (⇑ ρ) ∘ (⇑ σ)) x = (⇑ τ) x

theorem substComp' ρ σ τ (h : ∀ x, (subst ρ ∘ σ) x = τ x) : ∀ s, (subst ρ ∘ subst σ) s = subst τ s

theorem renameToSubst ξ : ∀ s, rename ξ s = subst (var ∘ ξ) s

theorem renameLiftRename ξ a : rename succ (rename ξ a) = rename (lift ξ) (rename succ a)

theorem renameUpSubst σ a : rename succ (subst σ a) = subst (⇑ σ) (rename succ a)

theorem renameDist ξ a s : subst (rename ξ a +: var) (rename (lift ξ) s) = rename ξ (subst (a +: var) s)

theorem substDrop σ a b : subst (a +: σ) (rename succ b) = subst σ b

theorem substDropAll a b : b = subst (a +: var) (rename succ b)

theorem substUnion σ a s : subst (a +: σ) s = subst (a +: var) (subst (⇑ σ) s)

theorem substDist σ a s : subst (subst σ a +: var) (subst (⇑ σ) s) = subst σ (subst (a +: var) s)

theorem substToRename x s : subst (var x +: var) s = rename (x +: id) s

theorem inHere {Γ A A'} (e : A' = rename succ A) : (Γ ∷ A) ∋ 0 ∶ A'

theorem inThere {Γ x A A' B} (h : Γ ∋ x ∶ A) (e : A' = rename succ A) : Γ ∷ B ∋ succ x ∶ A'

theorem wRenameSucc {Γ A} : Γ ∷ A ⊢ succ ∶ Γ

theorem wRenameLift {ξ : ℕ → ℕ} {Γ Δ A}
  (h : Δ ⊢ ξ ∶ Γ) :
  Δ ∷ (rename ξ A) ⊢ lift ξ ∶ Γ ∷ A

theorem neNf {a} : ne a → nf a

theorem nfPars {a b} (r : a ⇒⋆ b) : nf a → nf b

theorem nePars {a b} (r : a ⇒⋆ b) : ne a → ne b

theorem wneWnf {a} : wne a → wnf a

theorem nfWnf {a} (nfa : nf a) : wnf a

theorem neWne {a} (nea : ne a) : wne a

theorem wnfRename {ξ a} : wnf (rename ξ a) → wnf a

theorem wneRename {ξ a} : wne (rename ξ a) → wne a

theorem wnfBwds {a b} (r : a ⇒⋆ b) : wnf b → wnf a

theorem wneBwds {a b} (r : a ⇒⋆ b) : wne b → wne a

theorem wnfFwds {a b} (r : a ⇒⋆ b) : wnf a → wnf b

theorem wneFwds {a b} (r : a ⇒⋆ b) : wne a → wne b

theorem wneVar {s} : wne (var s)

theorem wnfPi {a b} (wnfa : wnf a) (wnfb : wnf b) : wnf (pi a b)

theorem wnfAbs {a b} (wnfa : wnf a) (wnfb : wnf b) : wnf (abs a b)

theorem wneApp {b a} (wneb : wne b) (wnfa : wnf a) : wne (app b a)

theorem wnf𝒰 {b} (wnfb : wnf b) : wnf (𝒰 b)

theorem wne𝒰 {b} : wne (𝒰 b) → False

theorem wneExf {a b} (wnfa : wnf a) (wneb : wne b) : wne (exf a b)

theorem wnfLvl {b} (wnfb : wnf b) : wnf (lvl b)

theorem wnfLof {k} : wnf (lof k)

theorem wneLof {a j} (r : a ⇒⋆ lof j) (wnea : wne a) : False

theorem wnfAppInv {b s} : wnf (app b (var s)) → wnf b

theorem interp𝒰Eq {i} {I : ∀ j, j < i → Term → Prop} {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a) =
  (λ a ↦ (∃ j lt, c ⇒⋆ lof j ∧ I j lt a) ∨ wne a)

theorem interp𝒰Lt {j k : lc.L} {b} (lt : j < k) :
  (λ a ↦ (∃ i, ∃ (_ : i < j), b ⇒⋆ lof i ∧ ∃ P, ⟦ a ⟧ i ↘ P) ∨ wne a) =
  (λ a ↦ (∃ i, ∃ (_ : i < k), b ⇒⋆ lof i ∧ ∃ P, ⟦ a ⟧ i ↘ P) ∨ wne a)

theorem interpLvlEq {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a) =
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ c ⇒⋆ lof k) ∨ wne a)

theorem interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ i, I ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I b P} (h : ⟦ 𝒰 b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a)

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

theorem interpLvlInv {i I b P} (h : ⟦ lvl b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpsNe {i a} (nea : ne a) : ⟦ a ⟧ i ↘ wne

theorem interpsPi {i a b Pa P}
  (ha : ⟦ a ⟧ i ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i b} (wnfb : wnf b) :
  ⟦ 𝒰 b ⟧ i ↘ (λ a ↦ (∃ j, ∃ (_ : j < i), b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ wne

theorem interpsLvl {i b} (wnfb : wnf b) :
  ⟦ lvl b ⟧ i ↘ (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpDet' {i I a P Q} (hP : ⟦ a ⟧ i , I ↘ P) (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) : ⟦ a ⟧ j ↘ P

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i b P} (h : ⟦ 𝒰 b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j, ∃ (_ : j < i), b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

theorem interpsLvlInv {i b P} (h : ⟦ lvl b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpWnf {i I a P}
  (adq : ∀ {a P}, (⟦ a ⟧ i , I ↘ P) → CR P)
  (h : ⟦ a ⟧ i , I ↘ P) : wnf a

theorem adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

theorem interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

theorem transl {i j k : lc.L} (lt : i < j) (le : j ≤ k) : i < k

theorem transr {i j k : lc.L} (le : i ≤ j) (lt : j < k) : i < k

theorem interp𝒰Eq {i} {I : ∀ j, j < i → Term → Prop} {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a) =
  (λ a ↦ (∃ j lt, c ⇒⋆ lof j ∧ I j lt a) ∨ wne a)

theorem interp𝒰Lt {j k : lc.L} {b} (lt : j < k) : ∀ {a},
  (∃ i, ∃ (_ : i < j), b ⇒⋆ lof i ∧ ∃ P, ⟦ a ⟧ i ↘ P) ∨ wne a →
  (∃ i, ∃ (_ : i < k), b ⇒⋆ lof i ∧ ∃ P, ⟦ a ⟧ i ↘ P) ∨ wne a

theorem interpLvlEq {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a) =
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ c ⇒⋆ lof k) ∨ wne a)

theorem interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ j le, ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ j , (λ k lt ↦ I k (transl lt le)) ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ j, (λ k lt ↦ I k (transl lt le)) ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I b P} (h : ⟦ 𝒰 b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j lt, b ⇒⋆ lof j ∧ I j lt a) ∨ wne a)

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

theorem interpLvlInv {i I b P} (h : ⟦ lvl b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpsNe {i a} (nea : ne a) : ⟦ a ⟧ i ↘ wne

theorem interpsPi {i j a b Pa P}
  (le : j ≤ i) (ha : ⟦ a ⟧ j ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ j ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ j ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i b} (wnfb : wnf b) :
  ⟦ 𝒰 b ⟧ i ↘ (λ a ↦ (∃ j, ∃ (_ : j < i), b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ wne

theorem interpsLvl {i b} (wnfb : wnf b) :
  ⟦ lvl b ⟧ i ↘ (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) :
  ∃ Q, (∀ {b}, P b → Q b) ∧ ⟦ a ⟧ j ↘ Q

theorem interpsCumul' {i j a P Q} (le : i ≤ j) (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) :
  ∀ {b}, P b → Q b

theorem interpDet' {i I a P Q}
  (hP : ⟦ a ⟧ i , I ↘ P)
  (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i b P} (h : ⟦ 𝒰 b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j, ∃ (_ : j < i), b ⇒⋆ lof j ∧ ∃ P, ⟦ a ⟧ j ↘ P) ∨ wne a)

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

theorem interpsLvlInv {i b P} (h : ⟦ lvl b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpWnf {i I a P}
  (adq : ∀ {a P}, (⟦ a ⟧ i , I ↘ P) → CR P)
  (h : ⟦ a ⟧ i , I ↘ P) : wnf a

theorem adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

theorem interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

theorem parEqv {a b} (r : a ⇒ b) : a ≈ b

theorem parsEqv {a b} (r : a ⇒⋆ b) : a ≈ b

theorem convEqv {a b} : a ⇔ b → a ≈ b

theorem eqvConv {a b} (r : a ≈ b) : a ⇔ b

theorem wtfApp {Γ A B B' b a}
  (hpi : Γ ⊢ b ∶ pi A B)
  (ha : Γ ⊢ a ∶ A)
  (eB : B' = subst (a +: var) B) :
  Γ ⊢ app b a ∶ B'

theorem wtf𝒰Inv {Γ j 𝒰'}
  (h : Γ ⊢ 𝒰 j ∶ 𝒰') :
  ∃ k, 𝒰 k ≈ 𝒰'

theorem wtfPiInvA𝒰 {Γ A B 𝒰'}
  (h : Γ ⊢ pi A B ∶ 𝒰') :
  ∃ j, Γ ⊢ A ∶ 𝒰 j ∧ 𝒰 j ≈ 𝒰'

theorem wtfPiInvA {Γ A B 𝒰'}
  (h : Γ ⊢ pi A B ∶ 𝒰') :
  ∃ j, Γ ⊢ A ∶ 𝒰 j

theorem wtfPiInvB {Γ A B 𝒰'}
  (h : Γ ⊢ pi A B ∶ 𝒰') :
  ∃ j, Γ ∷ A ⊢ B ∶ 𝒰 j

theorem wtfPiInv𝒰 {Γ A B 𝒰'}
  (h : Γ ⊢ pi A B ∶ 𝒰') :
  ∃ j, 𝒰 j ≈ 𝒰'

theorem wtfAbsInv {Γ A' b C}
  (h : Γ ⊢ abs A' b ∶ C) :
  ∃ A B, Γ ∷ A ⊢ b ∶ B ∧ A ≈ A' ∧ pi A B ≈ C

theorem wtfMtyInv {Γ 𝒰'}
  (h : Γ ⊢ mty ∶ 𝒰') :
  ∃ k, 𝒰 k ≈ 𝒰'

theorem wtfLvlInv {Γ a 𝒰'}
  (h : Γ ⊢ lvl a ∶ 𝒰') :
  ∃ b k, Γ ⊢ a ∶ lvl b ∧ 𝒰 k ≈ 𝒰'

theorem wtfLofInv {Γ j 𝒰'}
  (h : Γ ⊢ lof j ∶ 𝒰') :
  ∃ k, lvl k ≈ 𝒰'

theorem wtWf {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : ⊢ Γ

theorem interpLvlEq {b c} (r : b ⇒ c) :
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a) =
  (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ c ⇒⋆ lof k) ∨ wne a)

theorem interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ i, I ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I a P} (h : ⟦ 𝒰 a ⟧ i , I ↘ P) :
  (∃ j lt, a ⇒⋆ lof j ∧ P = I j lt) ∨ (wne a ∧ P = wne)

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

theorem interpLvlInv {i I b P} (h : ⟦ lvl b ⟧ i , I ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpsWne {i a} (wnea : wne a) : ⟦ a ⟧ i ↘ wne

theorem interpsPi {i a b Pa P}
  (ha : ⟦ a ⟧ i ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i j} (lt : j < i) :
  ⟦ 𝒰 (lof j) ⟧ i ↘ (λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ wne

theorem interpsLvl {i b} (nfb : nf b) :
  ⟦ lvl b ⟧ i ↘ (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpDet' {i I a P Q} (hP : ⟦ a ⟧ i , I ↘ P) (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) : ⟦ a ⟧ j ↘ P

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i a P} (h : ⟦ 𝒰 a ⟧ i ↘ P) :
  (∃ j, j < i ∧ a ⇒⋆ lof j ∧ P = λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P) ∨ (wne a ∧ P = wne)

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

theorem interpsLvlInv {i b P} (h : ⟦ lvl b ⟧ i ↘ P) :
  wnf b ∧ P = (λ a ↦ (∃ j k, j < k ∧ a ⇒⋆ lof j ∧ b ⇒⋆ lof k) ∨ wne a)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  wne T ∨
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem interpWnf {i I a P}
  (adq : ∀ {a P}, (⟦ a ⟧ i , I ↘ P) → CR P)
  (h : ⟦ a ⟧ i , I ↘ P) : wnf a

theorem adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

theorem interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

theorem nfCBN {a b} (nfa : nf a) (r : a ⇒β b) : False

theorem valuePars {a b} (r : a ⇒⋆ b) (v : Value a) : Nonempty (Value b)

theorem evaluation {a A : Term} (h : ⬝ ⊢ a ∶ A) : ∃ b, a ⇒⋆ b ∧ Nonempty (Value b)

theorem closed {a A : Term} (h : ⬝ ⊢ a ∶ A) : ¬ wne a

theorem consistency {b} : ¬ ⬝ ⊢ b ∶ mty

theorem canon𝒰 {T j} (h : ⬝ ⊢ T ∶ 𝒰 j) :
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

theorem canonLvl {a k} (h : ⬝ ⊢ a ∶ lvl k) : ∃ j, a ⇒⋆ lof j

theorem soundness {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : Γ ⊨ a ∶ A

theorem consistency {b} : ¬ ⬝ ⊢ b ∶ mty

theorem canon𝒰 {T j} (h : ⬝ ⊢ T ∶ 𝒰 j) :
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ k, T ⇒⋆ lvl (lof k))

theorem canonLvl {a k} (h : ⬝ ⊢ a ∶ lvl k) : ∃ j, a ⇒⋆ lof j

theorem interpPiInv {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ (Pa : Term → Prop) (Pf : Term → (Term → Prop) → Prop),
    (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, Pf x Pb) ∧
    (∀ x Pb, Pf x Pb → ⟦ subst (x +: var) b ⟧ i, I ↘ Pb) ∧
    P = (λ f ↦ ∀ x Pb, Pa x → Pf x Pb → Pb (app f x))

theorem interp𝒰Inv {i I a P} (h : ⟦ 𝒰 a ⟧ i , I ↘ P) :
  ∃ j lt, a ⇒⋆ lof j ∧ P = I j lt

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = (λ _ ↦ False)

theorem interpLvlInv {i I a P} (h : ⟦ lvl a ⟧ i , I ↘ P) :
  ∃ k, a ⇒⋆ lof k ∧ P = (λ a ↦ ∃ j, a ⇒⋆ lof j ∧ j < k)

theorem interpStepInv {i I T P} (h : ⟦ T ⟧ i , I ↘ P) :
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ k, T ⇒⋆ lvl (lof k))

theorem interpsPi {i a b Pa P}
  (ha : ⟦ a ⟧ i ↘ Pa)
  (hb : ∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) :
  P = (λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)) →
  ⟦ pi a b ⟧ i ↘ P

theorem interps𝒰 {i j} (lt : j < i) :
  ⟦ 𝒰 (lof j) ⟧ i ↘ (λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P)

theorem interpsMty {i} : ⟦ mty ⟧ i ↘ (λ _ ↦ False)

theorem interpsLvl {i k} : ⟦ lvl (lof k) ⟧ i ↘ (λ a ↦ ∃ j, a ⇒⋆ lof j ∧ j < k)

theorem interpFwd {i I a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i , I ↘ P) : ⟦ b ⟧ i , I ↘ P

theorem interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwd {i a b P} (r : a ⇒ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ b ⟧ i ↘ P) : ⟦ a ⟧ i ↘ P

theorem interpsConv {i a b P} (r : a ⇔ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

theorem interpsBwdsP {i a x y P} (r : x ⇒⋆ y) (h : ⟦ a ⟧ i ↘ P) : P y → P x

theorem interpDet' {i I a P Q} (hP : ⟦ a ⟧ i , I ↘ P) (hQ : ⟦ a ⟧ i , I ↘ Q) : P = Q

theorem interpsDet' {i a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ i ↘ Q) : P = Q

theorem interpsCumul {i j a P} (lt : i < j) (h : ⟦ a ⟧ i ↘ P) : ⟦ a ⟧ j ↘ P

theorem interpsDet {i j a P Q} (hP : ⟦ a ⟧ i ↘ P) (hQ : ⟦ a ⟧ j ↘ Q) : P = Q

theorem interpPiInv' {i I a b P} (h : ⟦ pi a b ⟧ i , I ↘ P) :
  ∃ Pa, (⟦ a ⟧ i , I ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i , I ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i , I ↘ Pb) → Pb (app f x)

theorem interpsPiInv {i a b P} (h : ⟦ pi a b ⟧ i ↘ P) :
  ∃ Pa, (⟦ a ⟧ i ↘ Pa) ∧
    (∀ x, Pa x → ∃ Pb, ⟦ subst (x +: var) b ⟧ i ↘ Pb) ∧
    P = λ f ↦ ∀ x Pb, Pa x → (⟦ subst (x +: var) b⟧ i ↘ Pb) → Pb (app f x)

theorem interps𝒰Inv {i a P} (h : ⟦ 𝒰 a ⟧ i ↘ P) :
  ∃ j, j < i ∧ a ⇒⋆ lof j ∧ P = λ a ↦ ∃ P, ⟦ a ⟧ j ↘ P

theorem interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = (λ _ ↦ False)

theorem interpsLvlInv {i a P} (h : ⟦ lvl a ⟧ i ↘ P) :
  ∃ k, a ⇒⋆ lof k ∧ P = (λ a ↦ ∃ j, a ⇒⋆ lof j ∧ j < k)

theorem interpsStepInv {I T P} (h : ⟦ T ⟧ I ↘ P) :
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ k, T ⇒⋆ lvl (lof k))

theorem semSubstNil σ : σ ⊨ ⬝

theorem semSubstCons {Γ : Ctxt} {σ i a A P} :
  (⟦ subst σ A ⟧ i ↘ P) → P a →
  σ ⊨ Γ → a +: σ ⊨ Γ ∷ A

theorem wtRename {ξ : ℕ → ℕ} {Γ Δ} {a A : Term}
  (hξ : Δ ⊢ ξ ∶ Γ) (hΔ : ⊢ Δ) (h : Γ ⊢ a ∶ A) :
  Δ ⊢ rename ξ a ∶ rename ξ A

theorem wtWeaken {Γ k} {a A B : Term}
  (hΓ : ⊢ Γ) (hB : Γ ⊢ B ∶ 𝒰 k) (h : Γ ⊢ a ∶ A) :
  Γ ∷ B ⊢ rename succ a ∶ rename succ A

theorem wSubstUp {σ Δ Γ k A}
  (hA : Δ ⊢ subst σ A ∶ 𝒰 k)
  (h : Δ ⊢ σ ∶ Γ) :
  Δ ∷ subst σ A ⊢ ⇑ σ ∶ Γ ∷ A

theorem wSubstCons {Γ} {a A : Term}
  (h : Γ ⊢ a ∶ A) :
  Γ ⊢ a +: var ∶ Γ ∷ A

theorem wtMorph {σ : ℕ → Term} {Γ Δ} {a A : Term}
  (hσ : Δ ⊢ σ ∶ Γ) (hΔ : ⊢ Δ) (h : Γ ⊢ a ∶ A) :
  Δ ⊢ subst σ a ∶ subst σ A

theorem wtSubst {Γ} {a A b B : Term}
  (hb : Γ ⊢ b ∶ B) (h : Γ ∷ B ⊢ a ∶ A) :
  Γ ⊢ subst (b +: var) a ∶ subst (b +: var) A

theorem wtReplace {Γ} {A B c C k : Term}
  (e : A ≈ B)
  (hB : Γ ⊢ B ∶ 𝒰 k)
  (h : Γ ∷ A ⊢ c ∶ C) :
  Γ ∷ B ⊢ c ∶ C

theorem wtMem {Γ x A} (mem : Γ ∋ x ∶ A) (h : ⊢ Γ) : ∃ k, Γ ⊢ A ∶ 𝒰 k

theorem wtRegularity {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : ∃ k, Γ ⊢ A ∶ 𝒰 k

theorem wtfAbs {Γ} {A B b k : Term}
  (hpi : Γ ⊢ pi A B ∶ 𝒰 k)
  (hb : Γ ∷ A ⊢ b ∶ B) :
  Γ ⊢ abs A b ∶ pi A B

theorem wtPar {Γ} {a b A : Term} (r : a ⇒ b) (h : Γ ⊢ a ∶ A) : Γ ⊢ b ∶ A

theorem wtPars {Γ} {a b A : Term} (r : a ⇒⋆ b) (h : Γ ⊢ a ∶ A) : Γ ⊢ b ∶ A

theorem CBNpar {a b} : a ⇒β b → a ⇒ b

theorem wtMty {Γ} {b : Term} (v : Value b) (h : Γ ⊢ b ∶ mty) : False
</all_available_lemmas>

<local_ctx>
import «src».typing

open Nat

open Term

variable [LevelClass]

notation:40 Δ:41 "⊢" σ:41 "∶" Γ:41 => wSubst σ Γ Δ

inductive Value : Term → Type where
  | 𝒰 {k} : Value (𝒰 k)
  | pi {a b} : Value (pi a b)
  | abs {a b} : Value (abs a b)
  | mty : Value mty
  | lvl {k} : Value (lvl k)
  | lof {k} : Value (lof k)

section

inductive CBN : Term → Term → Prop where
  | β {b a c} : app (abs c b) a ⇒β subst (a +: var) b
  | app {b b' a} : b ⇒β  b' → app b a ⇒β app b' a
  | exf {a b b'} : b ⇒β b' → exf a b ⇒β exf a b'

end

infix:40 "⇒β" => CBN

infix:40 "⇒β⋆" => CBNs

@[simp] 
def valueType {a} (A : Term) : Value a → Prop
  | Value.𝒰 | Value.pi | Value.mty | Value.lvl => ∃ k, 𝒰 k ≈ A
  | Value.abs => ∃ B C, pi B C ≈ A
  | Value.lof => ∃ k, lvl k ≈ A
</local_ctx>

<target_theorem>
theorem wtProgress {a A : Term} (h : ⬝ ⊢ a ∶ A) : Nonempty (Value a) ∨ ∃ b, a ⇒β b :=
</target_theorem>

