no goals
α : Type u_1
σ : Type ?u.50240
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
a : α
l : List α
n : ℕ
⊢ (Nat.casesOn n (Nat.succ (encode a)) fun n => encode (List.get? l (ofNat ℕ n))) =
    encode (List.get? (a :: l) (ofNat ℕ n))
cases n <;> simp