proposition: Lemma subs_satc u s s' : satc (fv u) s s' -> subs s u =>R* subs s' u.
proof: Proof. intro ss'. apply subs_rel_mon_preorder_aeq; class. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)