Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff OD.agda @ 358:811152bf2f47

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 12:39:21 +0900
parents 08d94fec239c
children 2a8a51375e49
line wrap: on
line diff
--- a/OD.agda	Tue Jul 14 11:19:48 2020 +0900
+++ b/OD.agda	Tue Jul 14 12:39:21 2020 +0900
@@ -392,6 +392,7 @@
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅
         lemma {o∅} iφ = x<nx
         lemma (isuc {y} x) = lemma2 where
+            --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
             lemma0 : y o< next o∅
             lemma0 = lemma x
             lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))