proposition: Lemma well_founded_equiv : forall (A:Type) R R' (H:forall x y, R x y <-> R' x y), @well_founded A R <-> well_founded R'.
proof: Proof. intros A R R' H. split;intro H';apply Inclusion.wf_incl with (2:=H'). red;intros;rewrite H;auto. red;intros;rewrite <- H;auto. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)