I am not sure I understand how metamath guarantees a unique substitution at all times. For example, in the proof of `th1` in `demo0.mm`, the two following expressions need to be matched in step 32:
`|- ( P -> Q )` `|- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )` This can be done with two naive substitutions: P := `( t + 0 ) = t` Q := `( ( t + 0 ) = t -> t = t )` or P := `( t + 0 ) = t -> ( ( t + 0 ) = t` Q := `t = t )` Is there a rule / principle in Metamath I am missing that precludes the second ill-defined substitution? Thank you! -- 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/dc1c7fd7-3f0a-4aa7-bb30-2287b37fbaa5n%40googlegroups.com.
