proposition: Theorem K_dec_set : forall A:Set, (forall x y:A, {x = y} + {x <> y}) -> forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
proof: Proof. Proof fun A => K_dec_type (A:=A). Theorem eq_rect_eq_dec : forall A:Type, (forall x y:A, {x = y} + {x <> y}) -> forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. intros A eq_dec. apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)). Qed.