Continued the proof of UA -> FEXT. No success yet, though.