{motive : Qq.Impl.UnquoteState → Sort u} →
  ((mvars : List (Lean.Expr × Qq.Impl.MVarSynth)) →
      (levelSubst : Std.HashMap Lean.Expr Lean.Level) →
        (exprSubst : Std.HashMap Lean.Expr Lean.Expr) →
          (unquoted : Lean.LocalContext) →
            (exprBackSubst : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult) →
              (levelBackSubst : Std.HashMap Lean.Level Lean.Expr) →
                (abstractedFVars : Array Lean.FVarId) →
                  (levelNames : List Lean.Name) →
                    (mayPostpone : Bool) →
                      motive
                        { mvars := mvars, levelSubst := levelSubst, exprSubst := exprSubst, unquoted := unquoted,
                          exprBackSubst := exprBackSubst, levelBackSubst := levelBackSubst,
                          abstractedFVars := abstractedFVars, levelNames := levelNames, mayPostpone := mayPostpone }) →
    (t : Qq.Impl.UnquoteState) → motive t