{motive : Qq.Impl.PatVarDecl → Sort u} →
  (t : Qq.Impl.PatVarDecl) →
    ((ty : Option Q(Lean.Expr)) →
        (fvarId : Lean.FVarId) → (userName : Lean.Name) → motive { ty := ty, fvarId := fvarId, userName := userName }) →
      motive t