fact: Axiom thm_FILTER_MAP : forall {_35843 _35850 : Type'}, forall P : _35843 -> Prop, forall f : _35850 -> _35843, forall l : list _35850, (@FILTER _35843 P (@List.map _35850 _35843 f l)) = (@List.map _35850 _35843 f (@FILTER _35850 (@o _35850 _35843 Prop P f) l)).
imports: coq theory_hol types terms axioms