fact: Definition extract_dp u v s t := cdp v u /\ exists f, exists l1, exists l2, exists sigma, s = apply_subst sigma v /\ Term f l2 = apply_subst sigma u /\ refl_trans_clos (one_step_list (one_step R)) l2 l1 /\ Term f l1 = t.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)