fact: Axiom thm_FILTER_APPEND : forall {_35816 : Type'}, forall P : _35816 -> Prop, forall l1 : list _35816, forall l2 : list _35816, (@FILTER _35816 P (@List.app _35816 l1 l2)) = (@List.app _35816 (@FILTER _35816 P l1) (@FILTER _35816 P l2)).
imports: coq theory_hol types terms axioms