case h.h.h.h
α : Type u_1
f : Nat
n : List α
l : α
⊢ takeD f n l = takeDTR f n l
⊢ @takeD = @takeDTR
funext α f n l
no goals
case h.h.h.h
α : Type u_1
f : Nat
n : List α
l : α
⊢ takeD f n l = takeDTR f n l
simp [takeDTR, takeDTR_go_eq]