Small revisions in Metamorphism.agda.