TY - RPRT TI - Models for Metamath AU - Mario Carneiro PY - 2016 UR - https://arxiv.org/abs/1601.07699 ID - 1601.07699 ER -