Alternate proof of cleljust. Compared with cleljustALT, it uses nfv followed by equsexv instead of [ax-5] followed by equsexhv, so it uses the idiom \( \Finv x' \, \varphi \) instead of ph -> A. x ph to express nonfreeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004.) (Revised by Mario Carneiro, 21-Dec-2016.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)