proposition: Lemma commut_tc : R! @ S << S @ R!.
proof: Proof. intros x y H. destruct H as [z Hxy]. destruct (tc_split (proj1 Hxy)) as [z' Hz']. assert (SE : (S @ R#) z' y). apply commut_rtc. exists z. intuition. destruct SE as [x' Rx']. assert (SRx : (S @ R) x x'). apply commut. exists z'. intuition. destruct SRx as [y' Sy']. exists y'. split. intuition. apply tc_merge. exists x'. intuition. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)