proposition: Lemma rdp_step_incl : forall R R' R1 R2, @inclusion _ R R' -> @inclusion _ R1 R2 -> @inclusion _ (rdp_step (axiom (dp R)) R1) (rdp_step (axiom (dp R')) R2).
proof: Proof. intros R R' R1' R2' R_in_R' R1_in_R2 t1 t2 H. inversion H as [g k l' s'' l_R_l' Hm]; clear H; subst. apply Rdp_step with l'. apply refl_trans_incl with (one_step_list (one_step R1')); trivial. do 2 intro; apply one_step_list_incl. apply one_step_incl; assumption. inversion Hm as [u1 u2 sigma]; clear Hm; subst. apply instance. apply dp_incl with R; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)