proposition: Lemma WF_union_commut : WF R -> WF S -> R @ S << S @ R -> WF (R U S).
proof: Proof. intros R_wf S_wf commut. apply wf_transp_WF. rewrite transp_union. apply wf_union. intros x y. unfold transp. intros xy z yz. assert (a : (R@S) x z). exists y. fo. apply commut in a. fo. apply WF_wf_transp. hyp. apply WF_wf_transp. hyp. Qed.
imports: Coq(Lia Wellfounded.Union) CoLoR(SN RelUtil LogicUtil AccUtil NotSN_IS ClassicUtil LeastNat DepChoice)