proposition: Lemma R_var_comb : forall rules1 rules2, (forall l r, In (l,r) rules1 -> forall v, l <> Var v) -> (forall l r, In (l,r) rules2 -> forall v, l <> Var v) -> (forall (l r : term), In (l,r) (rules1 ++ rules2) -> forall v, l <> Var v).
proof: Proof. intros rules1 rules2 R1_var R2_var l r H v. destruct (in_app_or _ _ _ H) as [H' | H']; [apply (R1_var l r H' v) | apply (R2_var l r H' v)]. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)