proposition: Lemma refl_trans_clos_dec : forall (A : Type) eq_bool, (forall a b : A, match eq_bool a b with true => a = b | false => a <> b end) -> forall (R : relation A) Rlist, (forall a b, R a b <-> In (a,b) Rlist) -> forall a b, {refl_trans_clos R a b}+{~refl_trans_clos R a b}.
proof: Proof. intros A eq_bool eq_bool_ok R Rlist Rlist_ok a b. generalize (eq_bool_ok a b); destruct (eq_bool a b); [intro a_eq_b; subst; do 2 left | intro a_diff_b]. destruct (trans_clos_dec _ eq_bool_ok _ _ Rlist_ok a b) as [Hab | Hab]. left; right; assumption. right; intro K; inversion K; subst; [apply a_diff_b; apply eq_refl | apply Hab; assumption]. Defined.
imports: Coq(Setoid Relations List Utf8)