{α : Type u_1} →
  {σ : Type u_2} →
    [inst : PartialOrder α] →
      {motive : CFilter α σ → Sort u} →
        (t : CFilter α σ) →
          ((f : σ → α) →
              (pt : σ) →
                (inf : σ → σ → σ) →
                  (inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a) →
                    (inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b) →
                      motive
                        { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right }) →
            motive t