proposition: Fact opt_enum_t_vec X n (P : X -> Prop) : opt_enum_t P -> opt_enum_t (fun v : vec X n => forall p, P (vec_pos v p)).
proof: Proof. intros HP. induction n as [ | n IHn ]. + exists (fun _ => Some vec_nil). intros v; vec nil v; split. * exists 0; auto. * intros _ p; invert pos p. + generalize (opt_enum_t_prod HP IHn). apply opt_enum_t_image with (f := fun p => vec_cons (fst p) (snd p)). intros v; split. * vec split v with x; intros H; exists (x,v); simpl; split; auto; split. - apply (H pos0). - intros p; apply (H (pos_nxt p)). * intros ((x,w) & (H1 & H2) & ->). simpl fst in *; simpl snd in *. intros p; invert pos 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)