proposition: Theorem inj_right_sigma_point : forall (P:A -> Type) (y y':P x), sigmaI P x y = sigmaI P x y' -> y = y'.
proof: Proof. intros. cut (proj (sigmaI P x y) y = proj (sigmaI P x y') y). unfold proj. simpl in |- *. case (eq_dec_point x). intro e. elim e using K_dec_point; trivial. intros. unfold proj in H1. case n; trivial. case H0. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes