∀ {motive : Lean.Expr.ProdTree → Sort u} (t : Lean.Expr.ProdTree)
  (F_1 : (t : Lean.Expr.ProdTree) → Lean.Expr.ProdTree.below t → motive t),
  Lean.Expr.ProdTree.brecOn t F_1 = F_1 t (Lean.Expr.ProdTree.brecOn.go t F_1).2