proposition: Lemma filter_weak_red_ord : weak_reduction_ordering succ succ_eq -> weak_reduction_ordering fsucc fsucc_eq.
proof: Proof. intro. destruct H as [Hwf (Hsubs,Hcont)]. split. apply WF_filter. hyp. split. apply filter_subs_closed. hyp. apply filter_weak_cont_closed. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)