proposition: Lemma star_list_equiv_empty : forall R1 R2 l r, star _ (one_step_list (one_step (union _ (union _ R1 Empty_R) R2))) r l <-> star _ (one_step_list (one_step (union _ R1 R2))) r l.
proof: Proof. intros R1 R2 l r. apply star_equiv. clear;intros l r. apply one_step_list_equiv;clear. intros l r. rewrite (union_sym (union _ R1 Empty_R)). rewrite <- union_assoc. rewrite Empty_R_neutral_union_l. apply union_sym. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)