Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/Ordinals.agda @ 693:a3b7f1e0ca60
same problem again
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 11 Jul 2022 11:49:11 +0900 |
parents | 099ca2fea51c |
children | 7c39cae23803 |
line wrap: on
line diff
--- a/src/Ordinals.agda Mon Jul 11 05:50:49 2022 +0900 +++ b/src/Ordinals.agda Mon Jul 11 11:49:11 2022 +0900 @@ -26,7 +26,7 @@ <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) - o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 + o<-irr : { x y : ord } → ( lt lt1 : x o< y ) → lt ≡ lt1 TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x