proposition: Lemma union_fact A (R S : rel A) : R U R @ S << R @ S%.
proof: Proof. unfold incl. intros. destruct H. exists y; split; unfold clos_refl, union; auto. do 2 destruct H. exists x0; split; unfold clos_refl, union; auto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)