proposition: Lemma between_dp0 : (forall u v, cdp v u -> connect_approx (u0,v0) (u,v) -> connect_approx (u,v) (u0,v0) -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection v) (projection u)) -> forall t1 t2 t3 t4, Rdp0 t2 t1 -> refl_trans_clos Rdp' t3 t2 -> Rdp0 t4 t3 -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection t3) (projection t2).
proof: Proof. intros Hdp t1 t2 t3 t4 H21 H32 H43; apply between_dp0_aux3 with t1 t2 t3 t4; trivial. left. left. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)