proposition: Lemma red_rtc_incl_filter_red_rtc : red R # << filter_ord (red R' #).
proof: Proof. unfold inclusion. induction 1. apply incl_filter with (red R'%). apply rc_incl_rtc. apply red_incl_filter_red_rc. exact H. unfold filter_ord. apply rt_refl. unfold filter_ord. apply rt_trans with (filter y). apply IHclos_refl_trans1. apply IHclos_refl_trans2. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)