fact: Record rwr_rel (pi : F.Symb.A) : Type := mk_set { ident : nat; Rel : relation term; rules : list (term * term); REquiv : (forall l r, Rel r l <-> In (l,r) rules); RR_var : (forall l r, In (l,r) rules -> forall v, l <> Var v); RR_reg : (forall l r, In (l,r) rules -> forall v, In v (var_list r) -> In v (var_list l)); RP : (forall l r, In (l,r) rules -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) }.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)