proposition: Fact type_enum_t_pos n : type_enum_t (pos n).
proof: Proof. exists (fun i => match le_lt_dec n i with left _ => None | right H => Some (nat2pos H) end). intros p. exists (pos2nat p). destruct (le_lt_dec n (pos2nat p)) as [ H | H ]. + generalize (pos2nat_prop p); lia. + rewrite nat2pos_pos2nat; 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)