Theorem: ASCII.String.length_push (ASCII/Lemmas.lean)

State before:
s : ASCII.String
c : ASCII.Char
⊢ (s.push c).length = s.length + 1
Tactic:
simp [length]
State after:
no goals