∀ (s : String) (c : Char) (pos : String.Pos.Raw),
  String.Legacy.revPosOfAux s c pos =
    if h : pos = 0 then none
    else
      have this := ⋯;
      have pos := String.Pos.Raw.prev s pos;
      if (String.Pos.Raw.get s pos == c) = true then some pos else String.Legacy.revPosOfAux s c pos