fact: Definition ind_pack@{i} {A : Type@{i}} {B : A -> Type@{i}} {x : A} {p q : B x} (e : p = q) : @paths (sigma (fun x => B x)) (x, p) (x, q) := (pr2_inv_uip e).
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec