∀ {α : Type u_1} (motive : RegularExpression α → Prop) (x : RegularExpression α),
  (∀ (a : Unit), motive RegularExpression.zero) →
    (∀ (a : Unit), motive RegularExpression.epsilon) →
      (∀ (a : α), motive (RegularExpression.char a)) →
        (∀ (R S : RegularExpression α), motive (R.plus S)) →
          (∀ (R S : RegularExpression α), motive (R.comp S)) → (∀ (R : RegularExpression α), motive R.star) → motive x