Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
(an improper simultaneous substitution - when a variable appears on the left and right of a rule)
When there are global essential statements (i.e. loaded from external sources) and if an improper simultaneous substitution tries to replace a variable in one or few global essential statements this may lead to errors because global essential statements are read-only, mm-lamp doesn't modify them during the global substitution.
This should be fixed by prohibiting such substitutions.
(an improper simultaneous substitution - when a variable appears on the left and right of a rule)
When there are global essential statements (i.e. loaded from external sources) and if an improper simultaneous substitution tries to replace a variable in one or few global essential statements this may lead to errors because global essential statements are read-only, mm-lamp doesn't modify them during the global substitution.
This should be fixed by prohibiting such substitutions.