proposition: Lemma connect_extract_dp_aux : forall u1 v1 s1 t1 un vn sn, Rcdp s1 t1 -> Rcdp sn s1 -> extract_dp u1 v1 s1 t1 -> extract_dp un vn sn s1 -> are_connected cdp R (un,vn) (u1,v1).
proof: Proof. intros u1 v1 s1 t1 un vn sn H1 Hn. unfold extract_dp. intros [D1 [f [l1 [l2 [sigma [K1 [J1 [L1 E1]]]]]]]] [Dn [g [k1 [k2 [tau [K2 [J2 [L2 E2]]]]]]]]. exists sigma; exists tau; subst; repeat split; trivial. rewrite <- J2. rewrite <- E2; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)