proposition: Lemma simplification_K_uip_refl@{i j|} : forall {A : Type@{i}} `{UIP A} (x : A) {B : x = x -> Type@{j}} (p : B 1), simplification_K_uip x p 1 = p.
proof: Proof. intros. unfold simplification_K_uip, UIP_K. now rewrite uip_refl_refl. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec