 Proper substitution, in Metamath databases that support it, is a derived construct instead of one built into the Metamath language itself.The substitution rule makes no assumption about the logic system in use and only requires that the substitutions of variables are correctly done.Here is a detailed example of how this algorithm works.