proposition: Lemma list_filter_sig_filter (l : list A) : proj1_sig <$> list_filter_sig l = filter P l.
proof: Proof. induction l as [| a l IH]; [done |]. simpl; rewrite filter_cons. destruct (decide _); csimpl; by rewrite IH. Qed.
imports: stdpp(options)