Forget non-<> equality proofs in realizability stuff
Minor cleanup
Add UIP
Funext should be in inference mode; fix annotation problem for free vars
BinderEq should be in inference mode