Change lookupTy to prefer user-specified type hints; this fixes subst w/ OTT(?)

There's no way to take a term, and then decide what equation it
witnesses, if it witnesses one at all. So we need to hold on to typing
hints given by the user (to know, for instance, that \x -> refl is a
homotopy between (\x -> x) and itself).
Fixed the ensure* functions to account for resolved observational eqs
Some golfing