case rfind c ih =>
  simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
  intro h₁ hm₁ h₂ hm₂
  by_contra hz
  wlog h : z < z' with Hz
  case inr =>
    have : z' < z := lt_of_le_of_ne (not_lt.mp h) (Ne.symm hz)
    exact Hz (k := k) c ih h₂ hm₂ h₁ hm₁ (Ne.symm hz) this
  have : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c) := hm₂ z h
  rcases this with ⟨x, xz, hx⟩
  exact xz (ih hx h₁)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
c : Code (n✝ + 1)
ih :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
v : Fin n✝ → M
z z' : M
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
          z = z'
no goals