proposition: Lemma subs_seq u s s' : seq (fv u) s s' -> subs s u = subs s' u.
proof: Proof. intro ss'. apply subs_rel_mon_preorder; class. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)