fact: Variable W3 : well_founded (rdp_step (axiom (ddp R3)) (@union _ (@union _ R1 R3) (Pi pi V0 V1))).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)