∀ (C : Type u_1) (a : Option C),
  (fun x =>
        match x with
        | CategoryTheory.WithTerminal.of a => some a
        | CategoryTheory.WithTerminal.star => none)
      ((fun x =>
          match x with
          | some a => CategoryTheory.WithTerminal.of a
          | none => CategoryTheory.WithTerminal.star)
        a) =
    a