simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
      (∀ (i : Fin n),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
            (∀ (i : Fin n),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
              z = z'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) ![] (z :> fun i => x i)) (codeAux c) →
      (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) ![] (z' :> fun i => x i)) (codeAux c) →
            (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) → z = z'