proposition: Lemma approx_is_approx : forall uv uv', ~connect_approx uv uv' -> ~ trans_clos (are_connected cdp R) uv uv'.
proof: Proof. unfold connect_approx; intros u v H. intro H'; apply H; clear H. induction H' as [x y H1 | x y z H1 Hn]. apply comp_ok; assumption. apply Nat.le_trans with (comp y). apply comp_ok; assumption. assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)