proposition: Theorem inj_right_sigma {P : A -> Type@{i}} {y y':P x} : (x, y) = (x, y') -> y = y'.
proof: Proof. intros. cut (projs (x, y) y = projs (sigmaI P x y') y). unfold projs. case (eq_dec x x). intro e. elim e using K_dec. trivial. intros. case e; reflexivity. case X; reflexivity. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes