In a dependently typed language, these would be different sigma types. Specialisations of functions to them, and the corresponding proofs of correctness, could

In a dependently typed language, these would be different sigma types. Specialisations of functions to them, and the corresponding proofs of correctness, could be computed automatically over these sigma types, likely using techniques in automatic theorem proving and/or LLMs. Good question!