α : Type u_1
β : Type ?u.308289
γ : Type ?u.308292
σ : Type ?u.308295
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
d : α
⊢ Primrec₂ fun l n => Option.getD (List.get? l n) d
α : Type u_1
β : Type ?u.308289
γ : Type ?u.308292
σ : Type ?u.308295
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
d : α
⊢ Primrec₂ fun l n => List.getD l n d
simp only [List.getD_eq_getD_get?]
no goals
α : Type u_1
β : Type ?u.308289
γ : Type ?u.308292
σ : Type ?u.308295
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
d : α
⊢ Primrec₂ fun l n => Option.getD (List.get? l n) d
exact option_getD.comp₂ list_get? (const _)