Goal:
    X : Type  Y : Type  f : X → Y → Prop  b : Y
  ============================
   (All (λ a : X, f a b) [])


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