∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (_l₁ _l₂ : List α),
  (List.isSetoid α) _l₁ _l₂ →
    Quot.mk (⇑(List.isSetoid α)) (List.filter (fun b => decide (p b)) _l₁) =
      Quot.mk (⇑(List.isSetoid α)) (List.filter (fun b => decide (p b)) _l₂)