c : Char
cs : List Char
b e : Pos
⊢ go₁ cs (0 + c) (b + c) (e + c) = go₁ cs 0 b e
c : Char
cs : List Char
b e : Pos
⊢ go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e
simp [go₁, Pos.ext_iff, Nat.ne_of_lt add_csize_pos]
no goals
c : Char
cs : List Char
b e : Pos
⊢ go₁ cs (0 + c) (b + c) (e + c) = go₁ cs 0 b e
apply go₁_add_right_cancel