proposition: Lemma SN_commut : forall x, SN R x -> forall x', S x x' -> SN R x'.
proof: Proof. induction 1; intros. apply SN_intro. intros. assert ((S @ R) x y). exists x'. intuition. ded (commut H3). do 2 destruct H4. apply (H0 _ H4 _ H5). Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)