proposition: Lemma one_step_union_sym : forall l r, one_step (union _ R1 R2) r l <-> one_step (union _ R2 R1) r l.
proof: Proof. intros l r. apply one_step_equiv. intros. apply (union_sym R1 R2). Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)