proposition: Lemma ddp_step_incl : forall R1 R2, @inclusion _ R1 R2 -> @inclusion _ (ddp_step R1) (ddp_step R2).
proof: Proof. intros R1' R2' R1_in_R2 t1 t2 H. apply (rddp_step_incl R1' R2' R1' R2'); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)