Refactor type parameter handling

This refactors type parameter handling in preparation for more trait handling.

Specifically,

• type parameters are now separately quantified over in function types (like lifetime parameters) instead of being mashed in with the other parameters,
• we can partially instantiate the type parameters of a function,
• function type notations have been generalized,
• Call expressions now also take type parameter annotations (similar to lifetimes) that provide hints for how to instantiate the type parameters of the callee. These suggested instantiations are only used if proving the argument assignments and the precondition does not already determine them.

case_studies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v

@@ -27,7 +27,6 @@ Proof.
     clear. solve_goal with nia.
   }
   
-  all: solve_goal with nia.
   Unshelve. all: print_remaining_sidecond.
 Qed.
 End proof.