Update STYLE, incorporating wiki; close #468

This is false.  The `assert` tactic produces subterms that can't be inspected by the rest of the proof script, but they are transparent in the resulting proof term.