no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ get 0 (as {0 ↦ a}) = a
cases as <;> rfl
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
k : ℕ
as : List α
⊢ get (k + 1) (as {k + 1 ↦ a}) = a
cases as <;> simp [get_set]