proposition: Lemma rel_dec : forall (P : relation term) Plist, (forall u v, P v u <-> In (u,v) Plist) -> forall r l, {P r l}+{~P r l}.
proof: Proof. intros P Plist Plist_ok r l; revert P Plist_ok. induction Plist as [ | [u v] Plist]; intros P Plist_ok. right; intro H; rewrite Plist_ok in H; contradiction. generalize (eq_bool_ok r v); destruct (eq_bool r v). generalize (eq_bool_ok l u); destruct (eq_bool l u). intros; subst l r; left; rewrite Plist_ok; left; apply eq_refl. intros l_diff_u _; destruct (IHPlist (fun v' u' => P v' u' /\ In (u',v') Plist)) as [[Ok _] | Ko]. intros s t; split. intros [_ H]; exact H. intros H; split; [rewrite Plist_ok; right | ]; assumption. left; assumption. right; intro H; rewrite Plist_ok in H; simpl in H; destruct H as [H | H]. apply l_diff_u; injection H; intros; apply sym_eq; assumption. apply Ko; split; [rewrite Plist_ok; right | ]; assumption. intros r_diff_v; destruct (IHPlist (fun v' u' => P v' u' /\ In (u',v') Plist)) as [[Ok _] | Ko]. intros s t; split. intros [_ H]; exact H. intros H; split; [rewrite Plist_ok; right | ]; assumption. left; assumption. right; intro H; rewrite Plist_ok in H; simpl in H; destruct H as [H | H]. apply r_diff_v; injection H; intros; apply sym_eq; assumption. apply Ko; split; [rewrite Plist_ok; right | ]; assumption. Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)