proposition: Lemma one_step_list_union_sym : forall l1 l2, one_step_list (one_step (union _ R1 R2)) l1 l2 <-> one_step_list (one_step (union _ R2 R1)) l1 l2.
proof: Proof. intros l1 l2. apply one_step_list_equiv. intros. apply (union_sym R1 R2). Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)