Added implicit argument resolution to constant and expression generation. Meta-variables that have as type a proposition are now added to the list of constraints when performing type inference (with meta-vars).