simpa[code, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp,
  Matrix.comp_vecCons', ←Part.eq_some_iff] using models_codeAux hc y v
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
hc : c.eval f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
no goals