fact: Definition ddp R v u := dp R v u /\ (forall i p, subterm_at_pos u (i :: p) <> Some v).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)