{α : Type u_1} →
  {motive : Filter α → Sort u} →
    ((sets : Set (Set α)) →
        (univ_sets : Set.univ ∈ sets) →
          (sets_of_superset : ∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets) →
            (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets) →
              motive
                { sets := sets, univ_sets := univ_sets, sets_of_superset := sets_of_superset,
                  inter_sets := inter_sets }) →
      (t : Filter α) → motive t