You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
On the official website there is the wff theorem weq which is proved from the syntax definition wceq.
However the corresponding metamath-web page shows weq as a derivable statement https://metamath.tirix.org/mpests/weq, which does not match the official website and it is also not true in general.
EDIT: also the metamath-web page does not show its proof.
The text was updated successfully, but these errors were encountered:
On the official website there is the wff theorem weq which is proved from the syntax definition wceq.
However the corresponding metamath-web page shows
weq
as a derivable statement https://metamath.tirix.org/mpests/weq, which does not match the official website and it is also not true in general.EDIT: also the metamath-web page does not show its proof.
The text was updated successfully, but these errors were encountered: