{motive : Aesop.BuilderName → Sort u} →
  motive Aesop.BuilderName.apply →
    motive Aesop.BuilderName.cases →
      motive Aesop.BuilderName.constructors →
        motive Aesop.BuilderName.destruct →
          motive Aesop.BuilderName.forward →
            motive Aesop.BuilderName.simp →
              motive Aesop.BuilderName.tactic → motive Aesop.BuilderName.unfold → (t : Aesop.BuilderName) → motive t