proposition: Fact fin_t_finite_t X (P : X -> Prop) (Pirr : forall x (H1 H2 : P x), H1 = H2) : fin_t P -> finite_t (sig P).
proof: Proof. intros (l & Hl). destruct (@Forall_reif_t _ l P) as (m & Hm). + rewrite Forall_forall; intro; apply Hl. + exists m. intros (x & Hx). generalize Hx; intros H. rewrite Hl, <- Hm, in_map_iff in Hx. destruct Hx as (y & <- & Hy). eq goal Hy; f_equal. destruct y; simpl; f_equal; apply Pirr. 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)