proposition: Lemma stable_union R S : stable R -> stable S -> stable (R U S).
proof: Proof. intros subs_R subs_S s s' ss' t u [tu|tu]; subst s'. left. apply subs_R; auto. right. apply subs_S; auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)