proposition: Lemma trans_comp_ok : forall uv uv', trans_clos (are_connected cdp R) uv uv' -> forall n n', comp uv n -> comp uv' n' -> n <= n'.
proof: Proof. intros x y H; induction H as [x y H1 | x y z H1 Hn]. apply comp_ok; assumption. intros nx nz Hx Hz. destruct x as [ux vx]; destruct y as [uy vy]; destruct H1 as [sigma [sigma' [H1 [H2 H3]]]]. destruct (comp_def _ _ H1) as [ny Hy]. apply Nat.le_trans with ny. apply comp_ok with (ux,vx) (uy,vy). exists sigma; exists sigma'; split; [ | split]; assumption. assumption. assumption. apply IHHn; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp)