proposition: Lemma uip_refl_refl@{i} {A : Type@{i}} {E : UIP@{i} A} (x : A) : uip (x:=x) 1 1 = 1.
proof: Proof. apply UIP_shift@{i}. intros y e. apply uip@{i}. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes