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

comparison ordinal.agda @ 183:de3d87b7494f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix zf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Jul 2019 17:56:12 +0900
parents 11490a3170d4
children 65e1b2e415bb
comparison
equal deleted inserted replaced
182:9f3c0e0b2bc9 183:de3d87b7494f
341 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) 341 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
342 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 342 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
343 → ¬ p 343 → ¬ p
344 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 344 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
345 345
346