proposition: Theorem fin_t_dec Q : @fin_t X Q -> fin_t (fun x => P x /\ Q x).
proof: Proof. Proof using Pdec. intros (l & Hl). exists (filter (fun x => if Pdec x then true else false) l). intros x; rewrite filter_In, <- Hl. destruct (Pdec x); try tauto. split; try tauto. intros []; discriminate. Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec)