proposition: Lemma inj_right_pair_refl (P : A -> Type) (y : P x) : inj_right_pair (y:=y) (y':=y) eq_refl = eq_refl.
proof: Proof. unfold inj_right_pair. intros. unfold eq_rect. unfold proj. rewrite eq_dec_refl. unfold K_dec. simpl. unfold eq_proofs_unicity. subst proj. simpl. unfold nu_inv, comp, nu. simpl. unfold eq_ind, nu_left_inv, trans_sym_eq, eq_rect, nu_constant. rewrite eq_dec_refl. reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes