proposition: Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
proof: Proof. Proof (fun UIP_refl x P => @UIP_refl_on__Streicher_K_on x P (UIP_refl x)). Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) : Streicher_K_on_ p (fun h => x = rew -> [P] h in x) -> Eq_rect_eq_on p P x. Proof. intro Streicher_K; red; intros. apply Streicher_K. reflexivity. Qed.