case refl
l r : List Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ Iterator.curr { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } } =
    List.headD r default
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ Iterator.curr it = List.headD r default
cases h.out'
no goals
case refl
l r : List Char
h : ValidFor l r { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
⊢ Iterator.curr { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } } =
    List.headD r default
apply get_of_valid