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 -> match l0 with
                   | [] => None
                   | x :: _ => Some x
                   end = Some a)


DEBUG:Going to execute:
simpl; intros; Tactics.destruct_all_rec_calls;
            repeat (Tactics.destruct_conjs; simpl proj1_sig in *); subst *;
            Tactics.autoinjections; try Tactics.discriminates