proposition: Lemma pr2_uip_refl@{i| } {A : Type@{i}} {E : UIP A} (P : A -> Type@{i}) (x : A) (y : P x) : pr2_uip@{i} (@idpath _ (x, y)) = 1.
proof: Proof. unfold pr2_uip, simplification_sigma1_dep_dep. now rewrite uip_refl_refl. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec