(A : Type) `{DecidablePaths A} (x : A) (P : forall (d : Decidable (x = x)), Type) (Px : P (inl idpath)) : forall d, P d. Proof. rapply (decidable_true idpath). intro p. assert (r : (idpath = p)) by apply path_ishprop. by destruct r. Defined.
Require Import