notation < "hvbox(Σ ident i opt (: ty) break . p)"
right associative with precedence 20
-for @{ 'exists ${default
+for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p)}
@{\lambda ${ident i} . $p}}}.
interpretation "constructive exists" 'sigma \eta.x =
- (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
\ No newline at end of file
+ (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).