fact: Axiom thm_FILTER : forall {_34398 : Type'} (h : _34398) (P : _34398 -> Prop) (t : list _34398), ((@FILTER _34398 P (@nil _34398)) = (@nil _34398)) /\ ((@FILTER _34398 P (@cons _34398 h t)) = (@COND (list _34398) (P h) (@cons _34398 h (@FILTER _34398 P t)) (@FILTER _34398 P t))).
imports: coq theory_hol types terms axioms