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

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

class LevelClass where
  L : Type
  lc : LevelClasses L

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

Lean.Expr in Lean.Expr

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)

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

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

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

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

Nonempty in Init.Prelude

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

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

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

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

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 semSubst σ Γ := ∀ x a, In x a Γ → ∀ i P, (⟦ subst σ a ⟧ i ↘ P) → P (σ x)

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

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

WellFoundedRelation in Init.WF

Or.inr in Init.Prelude

Nat.zero in Init.Prelude

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

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

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

OrderBot in Mathlib.Order.BoundedOrder.Basic

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

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

Or in Init.Prelude

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

Preorder in Mathlib.Order.Defs.PartialOrder

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

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

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

def main : IO Unit :=
  pure ()

IsTrans in Mathlib.Order.Defs.Unbundled

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 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 semWf Γ := ∀ x A, In x A Γ → ∃ k, Γ ⊨ A ∶ 𝒰 k

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

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

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

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

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

Lean.Expr.isEq in Lean.Util.Recognizers

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

IsWellOrder in Mathlib.Order.RelClasses

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

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

Bool in Init.Prelude

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

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

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

propext in Init.Core

@[simp] def wnf (a : Term) : Prop := ∃ b, nf 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))
  | 𝒰 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

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'

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

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

IO in Init.System.IO

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

Unit in Init.Prelude

id in Init.Prelude

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

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 semWt Γ a A := ∀ σ, σ ⊨ Γ → ∃ i P, (⟦ subst σ A ⟧ i ↘ P) ∧ P (subst σ a)

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

Nat.succ in Init.Prelude

L in Archive.Hairer

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

NoMaxOrder in Mathlib.Order.Max

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

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

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

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

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)

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

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

Or.inl in Init.Prelude

Nat in Init.Prelude

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

Nat.sub in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem parRefl a : a ⇒ a

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

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

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

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 soundness {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : Γ ⊨ a ∶ A

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

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

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

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

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 interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

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

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

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

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

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 renameExt ξ ζ (h : ∀ x, ξ x = ζ x) : ∀ s, rename ξ s = rename ζ s

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

theorem wtfAbs {Γ} {A B b k : Term}
  (hpi : Γ ⊢ pi A B ∶ 𝒰 k)
  (hb : Γ ∷ A ⊢ b ∶ B) :
  Γ ⊢ abs A b ∶ pi A 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 wneApp {b a} (wneb : wne b) (wnfa : wnf a) : wne (app b a)

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 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 wnfLvl {b} (wnfb : wnf b) : wnf (lvl b)

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

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

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

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

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

theorem neNf {a} : ne a → nf a

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

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

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

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

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

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 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 nePars {a b} (r : a ⇒⋆ b) : ne a → ne 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 normalization {Γ} {a A : Term} (h : Γ ⊢ a ∶ A) : wnf a ∧ wnf A

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 interpLvlInv {i I a P} (h : ⟦ lvl a ⟧ i , I ↘ P) :
  ∃ k, a ⇒⋆ lof k ∧ P = (λ a ↦ ∃ j, a ⇒⋆ lof j ∧ j < k)

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

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

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

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

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

theorem wnfLof {k} : wnf (lof k)

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

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

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

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

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

theorem wtSafety {a b A : Term} (h : ⬝ ⊢ a ∶ A) (r : a ⇒β⋆ b) :
  Nonempty (Value b) ∨ ∃ c, b ⇒β c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 nfWnf {a} (nfa : nf a) : wnf a

theorem wtValue {Γ} {a A B : Term} (h : Γ ⊢ a ∶ A) (e : A ≈ B) : (v : Value a) → valueType B v

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

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

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

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

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

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

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 eqvConv {a b} (r : a ≈ b) : a ⇔ b

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

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 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 interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

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 interpsMtyInv {i P} (h : ⟦ mty ⟧ i ↘ P) : P = wne

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem wfMty : ⊢ ⬝ ∷ mty

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 wnfRename {ξ a} : wnf (rename ξ a) → wnf a

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

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

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

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

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 conv𝒰Inv {a b} : 𝒰 a ⇔ 𝒰 b → a ⇔ b

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

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

theorem semWeaken {Γ a A B}
  (ha : Γ ⊨ a ∶ A) :
  Γ ∷ B ⊨ rename succ a ∶ rename succ 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 wtf𝒰Inv {Γ j 𝒰'}
  (h : Γ ⊢ 𝒰 j ∶ 𝒰') :
  ∃ k, 𝒰 k ≈ 𝒰'

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

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

theorem convApp {b b' a a'} : b ⇔ b' → a ⇔ a' → app b a ⇔ app b' 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 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 interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : P = wne

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

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

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

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 interpsWnf {i a P} (h : ⟦ a ⟧ i ↘ P) : wnf a

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

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 substExt σ τ (h : ∀ x, σ x = τ x) : ∀ s, subst σ s = subst τ s

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

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

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

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

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

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

theorem interpsLvl {i b} (nfb : nf b) :
  ⟦ lvl b ⟧ i ↘ (λ 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 idid : ⬝ ⊢ (abs (app (app ((app (var 0) (lof 3))) (idType 3)) (abs (app (var 1) (var 0))))) ∶ (pi (idType 4) (idType 3))

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

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

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

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

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

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 adequacy {i a P} (h : ⟦ a ⟧ i ↘ P) : CR P

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 interpsFwd {i a b P} (r : a ⇒ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

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

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 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 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 interpsFwds {i a b P} (r : a ⇒⋆ b) (h : ⟦ a ⟧ i ↘ P) : ⟦ b ⟧ i ↘ P

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

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 wtReplace {Γ} {A B c C k : Term}
  (e : A ≈ B)
  (hB : Γ ⊢ B ∶ 𝒰 k)
  (h : Γ ∷ A ⊢ c ∶ C) :
  Γ ∷ B ⊢ c ∶ C

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

theorem wneWnf {a} : wne a → wnf a

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

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

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

theorem wneVar {s} : wne (var s)

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

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

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 evaluation {a A : Term} (h : ⬝ ⊢ a ∶ A) : ∃ b, a ⇒⋆ b ∧ Nonempty (Value b)

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

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

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

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

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 wtAbs {Γ} {b A B : Term} (v : Value b) (h : Γ ⊢ b ∶ pi A B) : ∃ a' b', b = abs a' b'

theorem convLvlMty {j} : ¬ lvl j ⇔ mty

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

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

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

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

theorem interpMtyInv {i I P} (h : ⟦ mty ⟧ i , I ↘ P) : 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 canon𝒰 {T j} (h : ⬝ ⊢ T ∶ 𝒰 j) :
  (∃ A B, T ⇒⋆ pi A B) ∨
  (∃ i, T ⇒⋆ 𝒰 i) ∨
  (T ⇒⋆ mty) ∨
  (∃ b, T ⇒⋆ lvl b)

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

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

theorem wtfMty : ⬝ ∷ mty ⊢ var 0 ∶ mty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 renameId s : rename id s = s

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

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 interpNeInv {i I a P} (h : ⟦ a ⟧ i , I ↘ P) :
  ne a → P = wne

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

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

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

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

theorem convRefl {a} : a ⇔ a
</all_available_lemmas>

<local_ctx>
import «src».reduction

open Term

variable [lc : LevelClass]

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

notation:40 "⟦" a "⟧" i "," I "↘" 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

notation:40 "⟦" a "⟧" i "↘" P => Interps i a P
</local_ctx>

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

