proposition: Lemma filter_sub : forall s t, filter (sub s t) = sub (filter_subs s) (filter t).
proof: Proof. intro. apply term_ind_forall with (P := fun t => filter (sub s t) = sub (filter_subs s) (filter t)); intros; simpl. refl. apply args_eq. rewrite !Vfilter_map, !Vmap_map. apply Vmap_eq. eapply Vforall_incl with (v2 := v). intros. eapply Vin_filter_elim_in. apply H0. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)