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. refl. simpl. apply args_eq. rewrite <- !Vmap_filter, !Vmap_map. apply Vmap_eq. eapply Vforall_incl with (v2 := v). intros. eapply Vfilter_in. apply H0. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)