proposition: Lemma filter_subs_closed : substitution_closed succ -> substitution_closed fsucc.
proof: Proof. unfold substitution_closed. intros. unfold filter_ord. rewrite !filter_sub. apply H. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)