{motive : Aesop.TreeRef → Sort u} →
  ((gref : Aesop.GoalRef) → motive (Aesop.TreeRef.goal gref)) →
    ((rref : Aesop.RappRef) → motive (Aesop.TreeRef.rapp rref)) →
      ((cref : Aesop.MVarClusterRef) → motive (Aesop.TreeRef.mvarCluster cref)) → (t : Aesop.TreeRef) → motive t