proposition: Theorem UIP_shift@{i} : forall {U : Type@{i}}, UIP_refl_@{i} U -> forall x:U, UIP_refl_@{i} (x = x).
proof: Proof. exact (fun U UIP_refl x => @UIP_shift_on U x (UIP_refl x)). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes