{m : Type → Type} →
  {motive : Lean.MonadRef m → Sort u} →
    ((getRef : m Lean.Syntax) →
        (withRef : {α : Type} → Lean.Syntax → m α → m α) → motive { getRef := getRef, withRef := withRef }) →
      (t : Lean.MonadRef m) → motive t