# Pastebin UMOVAgxq
uip : ∀ {ℓ} {A B : Set ℓ} (x y : A ≡ B) → x ≡ y
uip refl refl = refl