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

State before:
β : Type u_1
inst✝ : Encodable β
k e : ℕ
⊢ decode e = (decode e).bind (List.toVector k)
Tactic:
exact rfl
State after:
no goals