# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557540700 -32400
# Node ID 9829ba02877fb5bfcc79640db703f2b2dae3e5e0
# Parent  c12d964a04c06b62afc1687a6a73ee26b5449aa0
ZF in Agda