proposition: Lemma uip_refl_refl {A} {E : UIP A} (x : A) : uip (x:=x) eq_refl eq_refl = eq_refl.
proof: Proof. assert (Us:=UIP_shift). specialize (Us A). compute in Us. apply Us. intros. apply uip. Defined.
imports: Equations.Init Equations.Prop.Classes