right associative with precedence 80
for @{'sig $x $h}.
-interpretation "sub_eqType" 'sig x h =
- (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ x h).
+interpretation "sub_eqType" 'sig x h = (mk_sigma ? ? x h).
(* restricting an eqType gives an eqType *)
lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p.