{α : Type u} →
  {motive : RegularExpression α → Sort u_1} →
    (t : RegularExpression α) →
      motive RegularExpression.zero →
        motive RegularExpression.epsilon →
          ((a : α) → motive (RegularExpression.char a)) →
            ((a a_1 : RegularExpression α) → motive a → motive a_1 → motive (a.plus a_1)) →
              ((a a_1 : RegularExpression α) → motive a → motive a_1 → motive (a.comp a_1)) →
                ((a : RegularExpression α) → motive a → motive a.star) → motive t