α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r
rw [sublistsLen, ← sublistsLenAux_append]
no goals
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
rfl