Theorem nfequid

Bound-variable hypothesis builder for \( x' = x' \). This theorem tells us that any variable, including \( x' \), is effectively not free in \( x' = x' \), even though \( x' \) is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.)

Conclusion
\( \vdash \Finv y \, x' = x' \)
Proof
equid
nfth _