proposition: Lemma ddp_is_dp : forall R t1 t2, ddp R t1 t2 -> dp R t1 t2.
proof: Proof. intros R t2 t1 [H _]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)