proposition: Lemma approx_dec: forall uv uv', {connect_approx uv uv'}+{~connect_approx uv uv'}.
proof: Proof. intros uv uv'; unfold connect_approx. destruct (le_lt_dec (comp uv) (comp uv')). left; exact l. right; apply Nat.lt_nge; assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)