Fix lambdas standing in for equality proofs
Proper equating of equality types
Allow optional type annotation for refl
Update .pi files for OTT

Fin and thence Vec are still broken.
Make the evidence optional for Refl (tt is default)