proposition: Lemma simplify_ind_pack_elim@{i j|} {A : Type@{i}} {uip : UIP A} (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j}) (t : G 1) : simplified_ind_pack B x p G (simplify_ind_pack_inv B x p G t) = t.
proof: Proof. unfold simplified_ind_pack, simplify_ind_pack_inv. now destruct (pr2_uip_refl B x p). Qed.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec