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

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