proposition: Lemma between_dp0_aux3 : (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 t5 t6, Rdp0 t2 t1 -> refl_trans_clos Rdp' t3 t2 -> refl_trans_clos Rdp' t4 t3 -> refl_trans_clos Rdp' t5 t4 -> Rdp0 t6 t5 -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection t4) (projection t3).
proof: Proof. intros Hdp t1 t2 t3 t4 t5 t6 H21 H32 H43. inversion H43 as [u | u4 u3 H43']; clear H43. intros _ _; left. subst u3 u4; revert t1 t2 t5 t6 H21 H32; induction H43' as [t4 t3 H43 | t4 t t3 H4 H3]; intros t1 t2 t5 t6 H21 H32 H54 H65. apply between_dp0_aux2 with t1 t2 t5 t6; trivial. apply refl_trans_clos_is_trans with (projection t). apply between_dp0_aux2 with t1 t2 t5 t6; trivial. apply refl_trans_clos_is_trans with t3; trivial. right; assumption. apply IHH3 with t1 t2 t5 t6; trivial. apply refl_trans_clos_is_trans with t4; trivial. right; left; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)