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 ->
    ∥ P (k + 0) a ∥ ->
    forall (n : nat) (x : A),
    nth_error l n = Some x ->
    nth_error l n =
    match l0 with
    | [] => None
    | _ :: l1 => nth_error l1 n
    end)


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