proposition: Theorem UIP_shift_on (X : Type) (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 eq_trans_r with eq_refl; apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP eq_refl eq_refl) z) (eq_sym (UIP eq_refl eq_refl))). - destruct z. destruct (UIP _ _). reflexivity. - change (match eq_refl as y' in _ = x' return y' = y' -> Prop with | eq_refl => fun z => z = eq_refl end (eq_trans (eq_trans (UIP (eq_refl) (eq_refl)) z) (eq_sym (UIP (eq_refl) (eq_refl))))). destruct z. destruct (UIP _ _). reflexivity. Defined.
imports: Equations.Init Equations.Prop.Classes