proposition: Lemma sn_comm_sn : forall x, SN R x -> (forall y, R#1 x y -> SN S y) -> S@R << R!1@S#1 -> SN (R U S) x.
proof: Proof. intros x snr sns comm. assert (SN (R!1 U S!1) x) as sntr. apply sn_comm_sntr; trivial. apply (SN_incl (R!1 U S!1)). apply union_incl. intros a b. apply t1_step. intros a b. apply t1_step. hyp. Qed.
imports: Coq(Lia Wellfounded.Union) CoLoR(SN RelUtil LogicUtil AccUtil NotSN_IS ClassicUtil LeastNat DepChoice)