finish last bits/bytes thm (using destruct_exists to preserve names); use unicode composition / clear admits