Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 74:819da8c08f05
ordinal atomical successor?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Jun 2019 19:19:40 +0900 |
parents | dd430a95610f |
children | 8e8f54e7a030 |
line wrap: on
line diff
--- a/ordinal-definable.agda Sat Jun 01 18:17:24 2019 +0900 +++ b/ordinal-definable.agda Sat Jun 01 19:19:40 2019 +0900 @@ -360,7 +360,8 @@ lemma {oz} {ooz} lt = def-subst {suc n} {ord→od ooz} (o<→c< lt) refl diso union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y )) - union→ X y u xx | tri< a ¬b ¬c = {!!} + union→ X y u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) + union→ X y u xx | tri< a ¬b ¬c | () union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where lemma : {oX ou ooy : Ordinal {suc n}} → ou ≡ ooy → ou o< oX → ooy o< oX lemma refl lt = lt