Theorem: HMem.Encoding.encodeList_inj (HMem/Encoding/Basic.lean)

State before:
α : Type u_1
inst✝ : Encoding α Memory
head✝ : α
tail✝ : List α
⊢ encodeList [] = encodeList (head✝ :: tail✝) → [] = head✝ :: tail✝
Tactic:
simp[encodeList]
State after:
no goals

State before:
α : Type u_1
inst✝ : Encoding α Memory
head✝ : α
tail✝ : List α
⊢ encodeList (head✝ :: tail✝) = encodeList [] → head✝ :: tail✝ = []
Tactic:
simp[encodeList]
State after:
no goals

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