fact: Fixpoint filter (t : term) : term' := match t with | Var x => Var x | Fun f ts => Fun' f (Vfilter (pi f) (Vmap filter ts)) end.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)