"The demodulation rule takes an equality statement x = y and any sentence with a nested term that unifies with x and derives the same sentence with y substituted for the nexted term." "If b.a=c is inferred in the presence of (x^(-1))^(-1)=x, substitution immediately yields obviously related inferences such as (b^(-1))^(-1).a=c."