proposition: Lemma simplify_ind_pack@{i j|} {A : Type@{i}} {uip : UIP A} (B : A -> Type@{i}) (x : A) (p q : B x) (G : p = q -> Type@{j}) : (forall e : (x, p) = (x, q), opaque_ind_pack_inv G e) -> (forall e : p = q, G e).
proof: Proof. intros H. intros e. specialize (H (ind_pack e)). unfold opaque_ind_pack_inv in H. rewrite ind_pack_inv_equiv in H. apply H. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec