Overhaul of the type system for existentials: push existential witness check under implications using expression normalization; simplify rules for existential lambda (`efunction` and `ematch`) by delegating disjunctions to `let-in`.