What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$?
Note on notation:
The epsilon takes a propositional content and returns a proposition in the simply typed lambda calculus. The lambda pi calculus modulo is just the usual dependently typed lambda calculus that serves as the metalanguage of LF but with a set of reduction rules