have ih := encodek xs
α : Type u_1
inst : Alphabet α
x : α
xs : List α
⊢ decode (encode (x :: xs)) = x :: xs
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ decode (encode (x :: xs)) = x :: xs