induction hc generalizing y <;> simp [code, codeAux, models_iff]
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
hc : c.eval f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
case zero
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 0 ↔ 0 = Part.some y

case one
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 1 ↔ 1 = Part.some y

case add
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ + v j✝ ↔ v i✝ + v j✝ = y

case mul
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ * v j✝ ↔ v i✝ * v j✝ = y

case proj
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ ↔ v i✝ = y

case equal
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i✝ = v j✝ ∧ y = 1 ∨ ¬v i✝ = v j✝ ∧ y = 0 ↔ (v i✝).isEqNat (v j✝) = y

case lt
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i✝ < v j✝ ∧ y = 1 ∨ v j✝ ≤ v i✝ ∧ y = 0 ↔ (v i✝).isLtNat (v j✝) = y

case comp
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c✝ : Code n✝
d✝ : Fin n✝ → Code m✝
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c✝.eval f✝
a✝ : ∀ (i : Fin n✝), (d✝ i).eval (g✝ i)
a_ih✝¹ : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c✝) ↔ f✝ (Vector.ofFn v) = Part.some y
a_ih✝ :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d✝ i)) ↔ g✝ i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) e (y :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c✝)) ∧
        ∀ (i : Fin n✝),
          (Semiformula.Eval (standardModel ℕ) e (y :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d✝ i)))) ↔
    (Vector.mOfFn fun i => g✝ i (Vector.ofFn v)).bind f✝ = Part.some y

case rfind
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
c✝ : Code (n✝ + 1)
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : c✝.eval ↑f✝
a_ih✝ :
  ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c✝) ↔ ↑f✝ (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ ((Semiformula.Evalfm ℕ (y :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c✝)) ∧
      ∀ x < y,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel ℕ) ![x_1, x] (y :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c✝))) ↔
    (Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y