proposition: Lemma P_comb : forall pi rules1 rules2, (forall l r, In (l,r) rules1 -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) -> (forall l r, In (l,r) rules2 -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) -> (forall l r, In (l,r) (rules1 ++ rules2) -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))).
proof: Proof. intros rules1 rules2 pi P1 P2 l r H f. destruct (in_app_or _ _ _ H) as [H' | H']; [apply (P1 l r H' f) | apply (P2 l r H' f)]. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)