fact: Definition rwr_rel_empty pi : rwr_rel pi := mk_set pi 0 Empty_R nil Equiv_empty R_var_empty R_reg_empty (P_empty pi).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)