case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
c : Char
l r : List Char
it : Iterator
h : ValidFor (c :: l) r it
⊢ ValidFor l (c :: r) (Iterator.prev it)
cases h.out'
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this :
  String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len (List.reverse l) + csize c } =
    { byteIdx := utf8Len (List.reverse l) }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
have := prev_of_valid l.reverse c r
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this :
  String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len (List.reverse l) + csize c } =
    { byteIdx := utf8Len (List.reverse l) }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
simp at this
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := List.reverse l ++ c :: r }, i := { byteIdx := utf8Len l } }
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r)
    (Iterator.prev { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } })
simp [Iterator.prev, this]
no goals
case refl
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := List.reverse l ++ c :: r }, i := { byteIdx := utf8Len l } }
exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp)
no goals
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ { s := { data := List.reverse l ++ c :: r }, i := { byteIdx := utf8Len l } }.s.data = List.reverseAux l (c :: r)
simp [List.reverseAux_eq]
no goals
c : Char
l r : List Char
h :
  ValidFor (c :: l) r
    { s := { data := List.reverse (c :: l) ++ r }, i := { byteIdx := utf8Len (List.reverse (c :: l)) } }
this : String.prev { data := List.reverse l ++ c :: r } { byteIdx := utf8Len l + csize c } = { byteIdx := utf8Len l }
⊢ { s := { data := List.reverse l ++ c :: r }, i := { byteIdx := utf8Len l } }.i.byteIdx = utf8Len l
simp