proposition: Theorem fin_t_vec X P n : @fin_t X P -> fin_t (fun v : vec _ n => forall p, P (vec_pos v p)).
proof: Proof. intros HP. induction n as [ | n IHn ]. + exists (vec_nil :: nil). intros v; vec nil v; simpl; split; try tauto. intros _ p; invert pos p. + generalize (fin_t_prod HP IHn). apply fin_t_map with (f := fun c => vec_cons (fst c) (snd c)). intros v; vec split v with x; split. * intros H; exists (x,v); simpl; msplit 2; auto. - apply (H pos0). - intro; apply (H (pos_nxt _)). * intros ((x',v') & H1 & H2 & H3). simpl in H1, H2, H3. apply vec_cons_inv in H1. destruct H1 as (-> & ->). intros p; invert pos p; 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)