proposition: Lemma subs1_saeq u s s' : saeq (fv u) s s' -> subs1 s u ~~ subs1 s' u.
proof: Proof. intro ss'. apply subs1_rel_mon_preorder; class. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)