Goal:
    A : Type  B : Type  P : A → Type  f : B → A
  ============================
   (All P (rev_map f []))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>