proposition: Theorem K_dec_Type : forall A:Type, (forall x y:A, {x = y} + {x <> y}) -> forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
proof: Proof. intros A Xdec x P H p. elim p using K_dec. intros x0 y; destruct (Xdec x0 y) as [e | ne]. - now left. - now right. - assumption. Qed.
imports: Arith