∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} {f : List α → β} {r : List α → Filter β},
  Filter.Tendsto f (pure []) (r []) →
    (∀ (l : List α) (a : α),
        Filter.Tendsto f (nhds l) (r l) → Filter.Tendsto (fun p => f (p.1 :: p.2)) (nhds a ×ˢ nhds l) (r (a :: l))) →
      ∀ (l : List α), Filter.Tendsto f (nhds l) (r l)