Goal:
    T : Type -> Type  M : Monad T  A : Type  P : nat -> A -> Type
  ============================
   (forall (l0 : list A) (k : nat),
    (forall (n : nat) (x : A), nth_error l0 n = Some x -> T (∥ P (k + n) x ∥)) ->
    forall (a : A) (l : list A), a :: l = l0 -> nth_error l0 0 = Some a)


DEBUG:Going to execute:
simpl in *