proposition: Lemma Empty_R_neutral_union_r : forall R x y, union _ Empty_R R x y <-> R x y.
proof: Proof. intros R x y. split;[idtac|intro H;right;assumption]. inversion_clear 1;trivial. case H0. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)