proposition: Theorem fin_t_length X n : finite_t X -> fin_t (fun l => @length X l < n).
proof: Proof. intros HX. apply finite_t_fin_t_eq in HX. generalize finite_t_unit; intros H1. apply finite_t_fin_t_eq in H1. induction n as [ | n IHn ]. + exists nil; intros; split; try lia; intros []. + generalize (fin_t_sum H1 (fin_t_prod HX IHn)). apply fin_t_map with (f := fun c => match c with | inl _ => nil | inr (x,l) => x::l end). intros [ | x l ]; simpl. * split; try lia; exists (inl tt); auto. * split. - intros Hl; exists (inr (x,l)); simpl; msplit 2; auto; lia. - intros ([ [] | (y,m) ] & E & H); try discriminate. simpl in *; inversion E; subst; lia. 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)