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

State before:
α : Type u_1
inst✝ : Coding α Memory
head✝ : α
tl : List α
⊢ decodeList (encodeList (head✝ :: tl)) = some (head✝ :: tl)
Tactic:
simpa [encodeList, decodeList, rawDecodeList] using rawDecodeList_inv tl
State after:
no goals