A simple version of sig_rec

Comple the following definition:

Definition sig_rec_simple (A:Set) (P: A -> Prop) (B : Set) :
  (forall x, P x -> B) -> (sig P) -> B.

Solution

Look at This file