Goal:
  
  ============================
   (forall T : Type -> Type,
    Monad T ->
    forall (A : Type) (P : nat -> A -> Type) (Q : A -> Type),
    (forall (n : nat) (x : A), ∥ Q x ∥ -> T (∥ P n x ∥)) ->
    forall (l0 : list A) (n : nat) (a : A) (l : list A),
    a :: l = l0 ->
    ∥ All Q (a :: l) ∥ ->
    ∥ P n a ∥ -> ∥ Alli P (S n) l ∥ -> ∥ Alli P n (a :: l) ∥)


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;
            try (solve
             [ red; intros; Tactics.destruct_conjs; Tactics.autoinjections;
                Tactics.discriminates ])