@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "Sigma" 'sigma \eta.x =
- (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ x).
+interpretation "Sigma" 'sigma \eta.x = (sigma ? x).
let rec type_OF_SP F ≝
match F return λF.Type with