I see, thank you for the answer. For a moment I thought that it's some sort of arcane requirement I missed while reading the Metamath book :-)
Perhaps I should remove this error message. > It will be interesting to see comments from other people (and to see if there are any malicious ways to use this peculiarity), but in case it all works out well, may I suggest to modify the metamath program in a way such that these kinds of proofs would check, but the program would still show a warning message? That way we may eventually find out if there's any use to this behavior. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4c5f3cf4-01cc-4468-81ed-161864ebf3cd%40googlegroups.com.
