c : Char
cs : List Char
⊢ { data := extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + csize c } } = { data := c :: cs }
c : Char
cs : List Char
⊢ extract { data := c :: cs } 0 (endPos { data := c :: cs }) = { data := c :: cs }
simp [extract, Nat.ne_of_gt add_csize_pos]
case e_data
c : Char
cs : List Char
⊢ extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + csize c } = c :: cs
c : Char
cs : List Char
⊢ { data := extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + csize c } } = { data := c :: cs }
congr
no goals
case e_data
c : Char
cs : List Char
⊢ extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + csize c } = c :: cs
apply extract.go₁_zero_utf8Len