proposition: Lemma SN_union_commut t : (forall x, SN S x -> SN R x) -> SN S t -> R @ S << S @ R -> SN (R U S) t.
proof: Proof. intros h s c. apply Acc_transp_SN. rewrite transp_union. apply Acc_union. intros x y. unfold transp. intros xy z yz. assert (a : (R@S) x z). exists y. fo. apply c in a. fo. intros x hx. apply SN_Acc_transp. apply h. apply Acc_transp_SN. hyp. apply SN_Acc_transp. hyp. Qed.
imports: Coq(Lia Wellfounded.Union) CoLoR(SN RelUtil LogicUtil AccUtil NotSN_IS ClassicUtil LeastNat DepChoice)