simp[encodeList, Iff.intro (encodeList_inj lhs rhs) λ h ↦ h ▸ rfl]
α : Type u_1
inst✝ : Encoding α Memory
head✝¹ : α
lhs : List α
head✝ : α
rhs : List α
⊢ encodeList (head✝¹ :: lhs) = encodeList (head✝ :: rhs) → head✝¹ :: lhs = head✝ :: rhs
no goals