proposition: Lemma Empty_R_equiv_list : forall l r : term, Empty_R r l <-> In (l,r) nil.
proof: Proof. split. inversion 1. inversion 1. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)