fact: Definition is_primary_pi pi R := forall s t, R s t -> (forall f, ((symb_in_term f s = true -> f <> pi) /\ (symb_in_term f t = true -> f <> pi))).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)