Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/ODUtil.agda @ 854:14bd0c9ad267
csupf b is no good, because supf1 x is not in UnionCF x ( but UnionCD (supf x) )
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 06 Sep 2022 05:15:40 +0900 |
parents | ef5dde91fa80 |
children | 55ab5de1ae02 |