proposition: Lemma filter_trans : transitive succ -> transitive fsucc.
proof: Proof. intro. unfold transitive, filter_ord. intros. eapply H. apply H0. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)