proposition: Theorem inj_right_sigma : forall (P:A -> Type) (y y':P x), sigmaI P x y = sigmaI P x y' -> y = y'.
proof: Proof. intros. cut (projs (sigmaI P x y) y = projs (sigmaI P x y') y). unfold projs. case (eq_dec x x). intro e. elim e using pK_dec. trivial. intros. case n; trivial. case H0. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes