proposition: Lemma inj_right_sigma_refl (P : A -> Type@{i}) (y : P x) : inj_right_sigma (y:=y) (y':=y) 1 = (id_refl _).
proof: Proof. unfold inj_right_sigma. intros. unfold eq_rect. unfold projs. destruct (id_sym@{i} eq_dec_refl). unfold K_dec. simpl. unfold eq_proofs_unicity. subst projs. simpl. unfold nu_inv, comp, nu. simpl. unfold eq_ind, nu_left_inv, trans_sym_eq, eq_rect, nu_constant. destruct (id_sym@{i} eq_dec_refl). reflexivity. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes