 So the verification is finished and these two steps of the proof of codice_12 are correct.When Metamath unifies with it has to check that the syntactical rules are respected.In fact has the type codice_22 thus Metamath has to check that is also typed codice_22.