Type Inference

[DanilaFe]

Once we have a unification function for terms (#3), we can proceed to type inference. We want to be able to, as much as possible,
to avoid writing down types. This is especially important for polymorphic functions, which, in the core Calculus of Inductive Constructions, require their type parameters to be explicitly provided at the call site.