fix bug in term_to_cert

in the lambda case, it would leave the assumption constraining the term
valuation on the bound variable (which comes when translating the body
of the lambda where the variable is free) on the final theorem
unnecessarily.
prove the onto and one_one interpretations using term_to_cert
show how we could have a matching select if we had range_to_in

but the problem is that range_to_in doesn't seem to be able to be
polymorphic enough... I'm not convinced there isn't a way to make it
work but it will be tricky. Is there a proof that this can never work?