simpa [encodeOp_succDef] using λ _ ↦ encodeOp_injN
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin (N₀ + 1) → Bool) → α
f₁ : (Fin (N₁ + 1) → Bool) → α
⊢ encode f₀ = encode f₁ → N₀ + 1 = N₁ + 1
no goals