fact: Fixpoint map_filter {A B: Type} (F: A -> option B ) (l: list A) : list B := match l with | nil => nil | e::l => match F e with | None => map_filter F l | Some e' => e' :: map_filter F l end end.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause