Theorem: Encodable.encode_list (Logic/Vorspiel/Computability.lean)

State before:
β : Type u_1
inst✝ : Encodable β
l : List β
⊢ encode l = encode (List.map encode l)
Tactic:
induction l <;> simp[*]
State after:
no goals