I am personally against using `Focus` in finished proof scripts.  Do you actually need it here, or can you re-order your proof?  (Also, consider using bullets (`-`) or braces (`{ <proof script here> }`) to organize long proofs like this.)