proposition: Lemma SN_red_supterm : forall x, SN (red R) x -> SN (red R U supterm) x.
proof: Proof. intros x snx. apply sn_comm_sn; trivial. intros y _. apply WF_supterm. clear. intros x y xy. assert ((red R @ supterm) x y) as [z [xz zy]]. apply supterm_red. hyp. exists z. split. apply t1_step. hyp. apply rt1_trans with y. hyp. apply rt1_refl. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)