proposition: Theorem UIP_shift_on@{i} (X : Type@{i}) (x : X) : UIP_refl_on_ X x -> forall y : x = x, UIP_refl_on_ (x = x) y.
proof: Proof. intros UIP_refl y. rewrite (UIP_refl y). intros z. assert (UIP:forall y' y'' : x = x, y' = y''). { intros. apply Id_trans_r with 1; apply UIP_refl. } transitivity (concat (concat (UIP 1 1) z) (inverse (UIP 1 1))). - destruct z. destruct (UIP _ _). reflexivity. - change (match 1 as y' in _ = x' return y' = y' -> Type@{i} with | 1 => fun z => z = 1 end (concat (concat (UIP 1 1) z) (inverse (UIP (1) (1))))). destruct z. destruct (UIP _ _). reflexivity. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Classes