-definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
-definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
+definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.\ 5a title="Sigma" href="cic:/fakeuri.def(1)"\ 6Σ\ 5/a\ 6x:A.P x ≝ λA,P,a,p. \ 5a href="cic:/matita/basics/types/Sig.con(0,1,2)"\ 6dp\ 5/a\ 6 … a p.
+definition eject : ∀A.∀P: A → Prop.(\ 5a title="Sigma" href="cic:/fakeuri.def(1)"\ 6Σ\ 5/a\ 6x:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].