{motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
            (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
              ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                    Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                  ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                    ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                      ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                        ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                          motive_6 t