cases (encodeOp_injN h)
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin N₀ → Bool) → α
f₁ : (Fin N₁ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₁ ∧ HEq f₀ f₁
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₀ ∧ HEq f₀ f₁