proposition: Theorem UIP_K@{i j} {A : Type@{i}} {U : UIP A} (x : A) : forall P : x = x -> Type@{j}, P 1 -> forall p : x = x, P p.
proof: Proof. intros P peq e. now elim (uip 1 e). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes