proposition: Lemma rtc_split_eq A (R : rel A) : R# == eq U R!.
proof: Proof. split. apply rtc_split. rewrite union_incl_eq. split. intros x y h. subst. refl. apply tc_incl_rtc. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)