proposition: Fact finite_t_fin_t_dec (X : Type) (P : X -> Prop) (Pdec : forall x, { P x } + { ~ P x }) : finite_t X -> fin_t P.
proof: Proof. intros H. apply finite_t_fin_t_eq in H. apply fin_t_dec with (1 := Pdec) in H. revert H; apply fin_t_equiv; tauto. 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)