-interpretation "constructive exists" 'exists \eta.x =
- (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
-interpretation "constructive exists (Type)" 'exists \eta.x =
- (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x).
+interpretation "constructive exists" 'exists \eta.x = (ex ? x).
+interpretation "constructive exists (Type)" 'exists \eta.x = (exT ? x).