fact: Fixpoint list_filter_sig (l : list A) : list (sig P) := match l with | [] => [] | x :: l => match decide (P x) with | left H => x ↾ H :: list_filter_sig l | _ => list_filter_sig l end end.
imports: stdpp(options)