proposition: Theorem finite_t_weak_dec_rels X : finite_t X -> { ll | forall R, (forall x y : X, R x y \/ ~ R x y) -> exists T, T ∈ ll /\ forall x y, R x y <-> T x y }.
proof: Proof. intros h. destruct finite_t_weak_dec_powerset with (h := finite_t_prod h h) as (l & _ & Hl). exists (map (fun P x y => P (x,y)) l). intros R HR. destruct (Hl (fun c => R (fst c) (snd c))) as (T & H1 & H2). + intros []; apply HR. + exists (fun x y => T (x,y)); split. * apply in_map_iff; exists T; auto. * intros x y; apply (H2 (x,y)). Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list fin_base)