proposition: Lemma rwr_equiv : forall r l, rwr R3 r l <-> rwr R4 r l.
proof: Proof. intros r l. split; apply trans_incl. intros t1 t2 H; rewrite <- one_step_equiv; assumption. intros t1 t2 H; rewrite one_step_equiv; assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)