simp [h]
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
h : v 0 = π₁ v 1
⊢ v 1 = ⟪v 0, π₂ v 1⟫
no goals