proposition: Lemma inj_sigma_r_refl@{i} (A : Type@{i}) (H : HSet A) (P : A -> Type@{i}) x (y : P x) : inj_sigma_r (y:=y) (y':=y) 1 = (id_refl _).
proof: Proof. unfold inj_sigma_r. intros. simpl. now rewrite is_hset_refl. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes