Theorem: length (Test/String/Length.lean)

State before:
⊢ "a".length = 1
Tactic:
rfl
State after:
no goals