proposition: Lemma inj_right_sigma_refl (P : A -> Type) (y : P x) : inj_right_sigma (y:=y) (y':=y) eq_refl = eq_refl.
proof: Proof. unfold inj_right_sigma. intros. unfold eq_rect. unfold projs. rewrite peq_dec_refl. unfold pK_dec. simpl. unfold peq_proofs_unicity. subst projs. simpl. unfold nu_inv, comp, nu. simpl. unfold eq_ind, nu_left_inv, ptrans_sym_eq, eq_rect, nu_constant. rewrite peq_dec_refl. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes