ZF-Resid

Redex

Substitution

Residuals

Reduction

Confluence