match s return λs.P (pi1 ? ? s) with
[ sigma_intro _ p ⇒ p].
-notation "hvbox(Σ ident i opt (: ty) break . p)"
+notation "hvbox(\Sigma ident i opt (: ty) break . p)"
right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p}