Theorem: LList.eval_cons_zero (GMLInit/Data/List/LList.lean)

State before:
α : Sort u_1
n : Nat
a : α
as : LList α n
⊢ (a :: as).eval (Fin.zero ⋯) = a
Tactic:
simp only [Fin.zero, LList.eval]
State after:
no goals