case refl
l m r : List Char
it₂ : Iterator
h₂ : ValidFor (List.reverse m ++ l) r it₂
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
⊢ Iterator.extract { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } } it₂ = { data := m }
l m r : List Char
it₁ it₂ : Iterator
h₁ : ValidFor l (m ++ r) it₁
h₂ : ValidFor (List.reverse m ++ l) r it₂
⊢ Iterator.extract it₁ it₂ = { data := m }
cases h₁.out
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (List.reverse m ++ l) r
    { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } }
⊢ Iterator.extract { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
      { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } } =
    { data := m }
case refl
l m r : List Char
it₂ : Iterator
h₂ : ValidFor (List.reverse m ++ l) r it₂
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
⊢ Iterator.extract { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } } it₂ = { data := m }
cases h₂.out
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (List.reverse m ++ l) r
    { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } }
⊢ String.extract { data := List.reverse l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len m + utf8Len l } =
    { data := m }
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (List.reverse m ++ l) r
    { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } }
⊢ Iterator.extract { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
      { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } } =
    { data := m }
simp [Iterator.extract, List.reverseAux_eq, Nat.not_lt.2 (Nat.le_add_left ..)]
no goals
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := List.reverseAux l (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (List.reverse m ++ l) r
    { s := { data := List.reverseAux (List.reverse m ++ l) r }, i := { byteIdx := utf8Len (List.reverse m ++ l) } }
⊢ String.extract { data := List.reverse l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len m + utf8Len l } =
    { data := m }
simpa [Nat.add_comm] using extract_of_valid l.reverse m r