case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ ValidFor l (List.modifyHead (fun x => c) r)
    (setCurr { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } } c)
l r : List Char
c : Char
it : Iterator
h : ValidFor l r it
⊢ ValidFor l (List.modifyHead (fun x => c) r) (setCurr it c)
cases h.out'
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ ValidFor l
    (match r with
    | [] => []
    | a :: l => c :: l)
    { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ ValidFor l (List.modifyHead (fun x => c) r)
    (setCurr { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } } c)
simp [Iterator.setCurr]
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ ValidFor l
    (match r with
    | [] => []
    | a :: l => c :: l)
    { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }
refine .of_eq _ ?_ (by simp)
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
this :
  set { data := List.reverse l ++ r } { byteIdx := utf8Len (List.reverse l) } c =
    { data := List.reverse l ++ List.modifyHead (fun x => c) r }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
have := set_of_valid l.reverse r c
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
this :
  set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c =
    {
      data :=
        List.reverse l ++
          match r with
          | [] => []
          | a :: l => c :: l }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
this :
  set { data := List.reverse l ++ r } { byteIdx := utf8Len (List.reverse l) } c =
    { data := List.reverse l ++ List.modifyHead (fun x => c) r }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
simp at this
no goals
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
this :
  set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c =
    {
      data :=
        List.reverse l ++
          match r with
          | [] => []
          | a :: l => c :: l }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    List.reverseAux l
      (match r with
      | [] => []
      | a :: l => c :: l)
simp [List.reverseAux_eq, this]
no goals
l r : List Char
c : Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ { s := set { data := List.reverse l ++ r } { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.i.byteIdx =
    utf8Len l
simp