(motive : Lean.Expr → List Lean.Elab.Term.LVal → Sort u_1) →
  (x : Lean.Expr) →
    (x_1 : List Lean.Elab.Term.LVal) →
      ((f : Lean.Expr) → motive f []) →
        ((f : Lean.Expr) →
            (lval : Lean.Elab.Term.LVal) → (lvals : List Lean.Elab.Term.LVal) → motive f (lval :: lvals)) →
          motive x x_1