simpa [encodeOp,
  λ b ↦ Iff.intro
    (encodeOp_inj
      (f₀ ∘ (Fin.cons (α := λ _ ↦ Bool) b))
      (f₁ ∘ (Fin.cons (α := λ _ ↦ Bool) b)))
    (λ h ↦ h ▸ rfl)]
  using λ hf ht ↦ funext λ y ↦ Fin.cons_self_tail y ▸
    match y 0 with
    | false => congrFun hf (Fin.tail y)
    | true => congrFun ht (Fin.tail y)
α : Type u_1
inst✝ : Encoding α Memory
N : ℕ
f₀ f₁ : (Fin (N + 1) → Bool) → α
⊢ encodeOp f₀ = encodeOp f₁ → f₀ = f₁
no goals