proposition: Fact Forall_reif_t X l (P : X -> Prop) : Forall P l -> { m : list (sig P) | map (@proj1_sig _ _) m = l }.
proof: Proof. induction l as [ | x l IHl ]. + exists nil; auto. + intros H; rewrite Forall_cons_inv in H. destruct H as (H1 & H2). destruct (IHl H2) as (m & Hm). exists (exist _ x H1 :: m); simpl; f_equal; auto. 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)