proposition: Lemma Empty_R_reg : (forall l r, In (l,r) nil -> forall v, In v (var_list r) -> In v (var_list l)).
proof: Proof. intros l r lr_in_nil; case lr_in_nil. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)