no goals
ι : Type ?u.503158
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
x : α
xs : List α
d✝ : α
n✝ : ℕ
l l' : List α
d : α
n : ℕ
h : n < length l
h' : optParam (n < length (l ++ l')) (_ : n < length (l ++ l'))
⊢ getD (l ++ l') n d = getD l n d
rw [getD_eq_get _ _ h', get_append _ h, getD_eq_get]