Add Subsorts to be able to make proofs over generic functions (useful for Proofs relating functional programming)