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