proposition: Lemma rc_filter_ord : inclusion (clos_refl fsucc) fsucc_eq.
proof: Proof. unfold inclusion, clos_refl, union, filter_ord. intros. decomp H. subst y. auto. auto. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)