∀ (T : Type u_1) (N : Type u_2),
  Function.RightInverse
    (fun x =>
      match x with
      | Symbol.terminal a => Sum.inl a
      | Symbol.nonterminal a => Sum.inr a)
    fun x =>
    match x with
    | Sum.inl a => Symbol.terminal a
    | Sum.inr a => Symbol.nonterminal a