proposition: Fact opt_enum_t_list X (P : X -> Prop) : opt_enum_t P -> opt_enum_t (Forall P).
proof: Proof. intros H. generalize (opt_enum_t_dep_sum _ _ eq_nat_dec type_enum_t_nat (fun n => opt_enum_t_vec n H)). apply opt_enum_t_image with (f := fun p => match p with existT _ n v => vec_list v end). intros l; rewrite Forall_forall; split. + intros Hl; exists (existT _ (length l) (list_vec l)); simpl. split. * intros p; apply Hl. rewrite <- (list_vec_iso l) at 3. apply in_vec_list, in_vec_pos. * rewrite list_vec_iso; auto. + intros ((n&v) & H1 & ->); simpl in *. intros x Hx; apply vec_list_inv in Hx. destruct Hx as (p & ->); auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops decidable)