∀ {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u}
  {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot))
  (F_1 : (t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
      Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t),
  Lean.Language.Lean.CommandParsedSnapshot.brecOn_1 t F_1 F_2 F_3 F_4 =
    F_2 t (Lean.Language.Lean.CommandParsedSnapshot.brecOn_1.go t F_1 F_2 F_3 F_4).2