proposition: Lemma star_equiv : forall (A:Type) (R1 R2: A -> A -> Prop), (forall l r, R1 r l <-> R2 r l) -> forall l r, star _ R1 r l <-> star _ R2 r l.
proof: Proof. intros A R1 R2 H l r. split;induction 1;try constructor. constructor 2 with y;auto. rewrite H in H1;assumption. constructor 2 with y;auto. rewrite H;assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)