chore: remove dead code at `Structure.lean`
1 file changed