definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
-
+
+(*
unification hint 0 ≔ C,P;
T ≟ carr C,
X ≟ DeqSig C P
X ≟ DeqSig T P
(* ---------------------------------------- *) ⊢
eq_sigma T P p1 p2 ≡ eqb X p1 p2.
-
+*)