∀ {α : Type u_1} (x : RegularExpression α),
  x.matches' =
    match x with
    | RegularExpression.zero => 0
    | RegularExpression.epsilon => 1
    | RegularExpression.char a => {[a]}
    | P.plus Q => P.matches' + Q.matches'
    | P.comp Q => P.matches' * Q.matches'
    | P.star => KStar.kstar P.matches'