(motive : Lean.Elab.Term.Do.Code → Sort u_1) →
  (x : Lean.Elab.Term.Do.Code) →
    ((ref val : Lean.Syntax) → motive (Lean.Elab.Term.Do.Code.return ref val)) →
      ((x : Lean.Elab.Term.Do.Code) → motive x) → motive x