# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564629866 -32400
# Node ID 6bb5d57c9561b336b32c6b2b6afed29f50c63fae
# Parent  f5b3f30fcb162a3f332dcf9c4e9e0a292c154d87# Parent  2c7d45734e3be59a06d272a07fecdbf77ab8ce10
Axiom of choice from exclude middle