proposition: Lemma P_empty : forall pi, forall l r, In (l,r) nil -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi))).
proof: Proof. intros pi l r H; case H. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)