Thank you, Mario There's also this footnote: This requirement can greatly simplify the unification algorithm (substitution calculation) required by proof verification.
(I need to check if I was anyway assuming this to be the case, or if my verification / unification code can improve using this assumption) -- 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/731de42e-f9e7-4f20-9043-bdd35f38b549n%40googlegroups.com.
