proposition: Lemma rwr_list_equiv : forall l1 l2, refl_trans_clos (one_step_list (one_step R3)) l1 l2 <-> refl_trans_clos (one_step_list (one_step R4)) l1 l2.
proof: Proof. intros l1 l2; split; apply refl_trans_incl. intros k1 k2 H; rewrite <- one_step_list_equiv; assumption. intros k1 k2 H; rewrite one_step_list_equiv; assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)