proposition: Lemma WF_compose_swap : WF (R @ S) -> WF (S @ R).
proof: Proof. intro WF_RS. assert (forall p q, R p q -> SN (S @ R) q). intro p. pattern p. apply SN_ind with A (R @ S); auto. intros. apply SN_intro. intros. destruct H2. apply H0 with x0. exists q; intuition. intuition. unfold WF. intro. apply SN_intro. intros. destruct H0 as [z [Sxz Rzy]]. apply H with z. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)