reg064.idr

sigmaEq2 : {A : Type} ->
           {P : A -> Type} ->
           {s1: DPair A P} ->
           {s2: DPair A P} ->
           fst s1 = fst s2 ->
           snd s1 = snd s2 ->
           s1 = s2
sigmaEq2 {A=a} {P=p} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl