fact: Parameter 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}.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)