Describir: Verificación formal del zipper relacional simétrico