-interpretation "constructive exists" 'exists \eta.x = (ex _ x).
-interpretation "constructive exists (Type)" 'exists \eta.x = (exT _ x).
+interpretation "constructive exists" 'exists \eta.x = (ex ? x).
+interpretation "constructive exists (Type)" 'exists \eta.x = (exT ? x).