Theorem: Strings.thm_2 (FOL/Parsing/Text.lean)

State before:
α : Type
s t u : Str α
⊢ s ++ (t ++ u) = s ++ t ++ u
Tactic:
symm
State after:
α : Type
s t u : Str α
⊢ s ++ t ++ u = s ++ (t ++ u)

State before:
α : Type
s t u : Str α
⊢ s ++ t ++ u = s ++ (t ++ u)
Tactic:
exact (List.append_assoc s t u)
State after:
no goals