proposition: Lemma SN_st_app_r u v : SN R (App u v) -> SN R v.
proof: Proof. intro h. eapply SN_st. apply h. apply st_app_r. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)