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