proposition: Theorem finite_t_weak_dec_powerset (h : finite_t X) : { ll | length ll = 2 ^ (length (proj1_sig h)) /\ forall R, wdec R -> exists T, T ∈ ll /\ forall x, R x <-> T x }.
proof: Proof. destruct h as (l & Hl). destruct (pset_fin_t l) as (ll & H & Hll). exists ll; split; auto. intros R HR. destruct (Hll _ HR) as (T & H1 & H2). exists T; split; auto. Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list fin_base)