(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/realisability/".
-
include "logic/connectives.ma".
include "datatypes/constructors.ma".
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}