proposition: Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.
proof: Proof. Proof (fun UIP x p => @UIP_on__UIP_refl_on x (UIP x x eq_refl) p). Lemma UIP_refl_on__Streicher_K_on (x : U) (P : x = x -> Prop) : UIP_refl_on_ x -> Streicher_K_on_ x P. Proof. intro UIP_refl; red; intros; rewrite UIP_refl; assumption. Qed.