proposition: Lemma one_step_list_equiv : forall r l, one_step_list (one_step R3) r l <-> one_step_list (one_step R4) r l.
proof: Proof. intros r l. split; apply one_step_list_incl. intros; rewrite <- one_step_equiv; assumption. intros; rewrite one_step_equiv; assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)