proposition: Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
proof: Proof. Proof (fun Streicher_K p P x => @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)). End Equivalences. Theorem UIP_shift_on (X : Type) (x : X) : UIP_refl_on_ X x -> forall y : x = x, UIP_refl_on_ (x = x) y. 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 x); apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. destruct (UIP _ _). reflexivity. - change (match eq_refl x as y' in _ = x' return y' = y' -> Prop with | eq_refl => fun z => z = (eq_refl (eq_refl x)) end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x))))). destruct z. destruct (UIP _ _). reflexivity. Qed.