Goal:
    A : Type  P : nat → A → Type  k : nat  X : Alli P k []
  ============================
   (Alli (λ _ : nat, P k) 0 [])


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