proposition: Lemma WF_red_supterm : WF (red R) -> WF (red R U supterm).
proof: Proof. intros h t. apply SN_red_supterm. apply h. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)