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