(motive : Lean.LocalContext × Std.HashMap Lean.FVarId Lean.Name → Sort u_1) →
  (__discr : Lean.LocalContext × Std.HashMap Lean.FVarId Lean.Name) →
    ((lctx : Lean.LocalContext) → (boundFVars : Std.HashMap Lean.FVarId Lean.Name) → motive (lctx, boundFVars)) →
      motive __discr