Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/BAlgebra.agda @ 1465:bd2b003e25ef
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Jan 2024 13:50:21 +0900 |
| parents | 484f83b04b5d |
| children | e8c166541c86 |
| rev | line source |
|---|---|
| 1464 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 431 | 2 open import Level |
| 3 open import Ordinals | |
| 1464 | 4 import HODBase |
| 5 import OD | |
| 6 module BAlgebra {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) | |
| 7 (AC : OD.AxiomOfChoice O HODAxiom ) | |
| 8 where | |
| 431 | 9 |
| 1464 | 10 -- open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 11 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 12 open import Data.Empty | |
| 13 open import Data.Unit | |
| 14 open import Relation.Nullary | |
| 15 open import Relation.Binary hiding (_⇔_) | |
| 16 open import Relation.Binary.Core hiding (_⇔_) | |
| 17 import Relation.Binary.Reasoning.Setoid as EqR | |
| 18 | |
| 431 | 19 open import logic |
| 20 import OrdUtil | |
| 1464 | 21 open import nat |
| 431 | 22 |
| 23 open Ordinals.Ordinals O | |
| 24 open Ordinals.IsOrdinals isOrdinal | |
| 1300 | 25 -- open Ordinals.IsNext isNext |
| 431 | 26 open OrdUtil O |
| 1464 | 27 import ODUtil |
| 28 open ODUtil O HODAxiom ho< | |
| 29 import ODC | |
| 431 | 30 |
| 1464 | 31 -- Ordinal Definable Set |
| 32 | |
| 1465 | 33 open HODBase.HOD |
| 34 open HODBase.OD | |
| 431 | 35 |
| 36 open _∧_ | |
| 37 open _∨_ | |
| 38 open Bool | |
| 39 | |
| 1464 | 40 open HODBase._==_ |
| 41 | |
| 1465 | 42 open HODBase.ODAxiom HODAxiom |
| 1464 | 43 open OD O HODAxiom |
| 44 open AxiomOfChoice AC | |
| 45 | |
| 46 open _∧_ | |
| 47 open _∨_ | |
| 48 open Bool | |
| 49 | |
| 1465 | 50 L＼L=0 : { L : HOD } → (L ＼ L) =h= od∅ |
| 1464 | 51 L＼L=0 {L} = record { eq→ = lem0 ; eq← = lem1 } where |
| 1123 | 52 lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x |
| 53 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx) | |
| 54 lem1 : {x : Ordinal} → odef od∅ x → odef (L ＼ L) x | |
| 55 lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
| 56 | |
| 1464 | 57 L＼Lx=x : { L x : HOD } → x ⊆ L → (L ＼ ( L ＼ x )) =h= x |
| 58 L＼Lx=x {L} {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 } where | |
| 1465 | 59 lem03 : {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z |
| 1464 | 60 lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O HODAxiom AC x (* z) |
| 1465 | 61 ... | yes y = subst (λ k → odef x k ) &iso y |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
62 ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ ) |
| 1465 | 63 lem04 : {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z |
| 1464 | 64 lem04 {z} xz with ODC.∋-p O HODAxiom AC L (* z) |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
65 ... | yes y = ⟪ subst (λ k → odef L k ) &iso y , ( λ p → proj2 p xz ) ⟫ |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
66 ... | no n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) )) |
| 1465 | 67 |
| 68 L＼0=L : { L : HOD } → (L ＼ od∅) =h= L | |
| 1464 | 69 L＼0=L {L} = record { eq→ = lem05 ; eq← = lem06 } where |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
70 lem05 : {x : Ordinal} → odef (L ＼ od∅) x → odef L x |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
71 lem05 {x} ⟪ Lx , _ ⟫ = Lx |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
72 lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
73 lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt) ⟫ |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
74 |
| 1182 | 75 ∨L＼X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x |
| 1464 | 76 ∨L＼X {L} {X} {x} Lx with ODC.∋-p O HODAxiom AC X (* x) |
| 1182 | 77 ... | yes y = case1 ( subst (λ k → odef X k ) &iso y ) |
| 78 ... | no n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫ | |
| 79 | |
| 1465 | 80 ＼-⊆ : { P A B : HOD } → A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B ) |
| 1241 | 81 ＼-⊆ {P} {A} {B} A⊆P = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx , (λ ax → proj2 pbx (a<b ax)) ⟫ ) , lem07 ⟫ where |
| 82 lem07 : (P ＼ B) ⊆ (P ＼ A) → A ⊆ B | |
| 1464 | 83 lem07 pba {x} ax with ODC.p∨¬p O HODAxiom AC (odef B x) |
| 1241 | 84 ... | case1 bx = bx |
| 85 ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax , ¬bx ⟫ ) ax ) | |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
86 |
| 1293 | 87 RC＼ : {L : HOD} → RCod (Power (Union L)) (λ z → L ＼ z ) |
| 1464 | 88 RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz ; ψ-eq = λ {x} {y} → wdf {x} {y} } where |
| 1293 | 89 lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L ) |
| 90 lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz } | |
| 1464 | 91 wdf : {x y : HOD} → od x == od y → (L ＼ x) =h= (L ＼ y) |
| 1465 | 92 wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫ |
| 1464 | 93 ; eq← = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq→ x=y yp) ) ⟫ } |
| 1293 | 94 |
| 95 | |
| 1464 | 96 [a-b]∩b=0 : { A B : HOD } → ((A ＼ B) ∩ B) =h= od∅ |
| 97 [a-b]∩b=0 {A} {B} = record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
| 451 | 98 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } |
| 99 | |
| 480 | 100 U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U |
| 1096 | 101 U-F=∅→F⊆U {F} {U} not = gt02 where |
| 480 | 102 gt02 : { x : Ordinal } → odef F x → odef U x |
| 1464 | 103 gt02 {x} fx with ODC.∋-p O HODAxiom AC U (* x) |
| 480 | 104 ... | yes y = subst (λ k → odef U k ) &iso y |
| 105 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) | |
| 106 | |
| 1464 | 107 ∪-Union : { A B : HOD } → Union (A , B) =h= ( A ∪ B ) |
| 1465 | 108 ∪-Union {A} {B} = ( record { eq→ = lemma4 ; eq← = lemma2 } ) where |
| 109 lemma4 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x | |
| 110 lemma4 {x} record { owner = owner ; ao = (case1 refl) ; ox = ox } = case1 (eq← *iso== ox) | |
| 111 lemma4 {x} record { owner = owner ; ao = (case2 refl) ; ox = ox } = case2 (eq← *iso== ox) | |
| 431 | 112 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x |
| 1284 | 113 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) A |
| 431 | 114 ⟪ case1 refl , d→∋ A A∋x ⟫ ) |
| 1284 | 115 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) B |
| 431 | 116 ⟪ case2 refl , d→∋ B B∋x ⟫ ) |
| 117 | |
| 1465 | 118 open import zf |
| 119 | |
| 120 pred-in : (A B : HOD ) → ZPred HOD _∋_ _=h=_ (λ x → (A ∋ x) ∧ (B ∋ x)) | |
| 121 pred-in A B = record { ψ-cong = wdf } where | |
| 122 wdf : (x y : HOD) → x =h= y → ((A ∋ x) ∧ (B ∋ x)) ⇔ ((A ∋ y) ∧ (B ∋ y)) | |
| 123 wdf = λ x y x=y | |
| 124 → ⟪ (λ p → ⟪ subst (λ k → odef A k) (==→o≡ x=y) (proj1 p) | |
| 125 , subst (λ k → odef B k) (==→o≡ x=y) (proj2 p) ⟫ ) | |
| 126 , (λ p → ⟪ subst (λ k → odef A k) (sym (==→o≡ x=y)) (proj1 p) | |
| 127 , subst (λ k → odef B k) (sym (==→o≡ x=y)) (proj2 p) ⟫ ) ⟫ | |
| 128 | |
| 129 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x )) (pred-in A B) =h= ( A ∩ B ) | |
| 1464 | 130 ∩-Select {A} {B} = record { eq→ = lemma1 ; eq← = lemma2 } where |
| 1465 | 131 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x → odef (A ∩ B) x |
| 431 | 132 lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫ |
| 1465 | 133 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x |
| 431 | 134 lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫ |
| 135 | |
| 1464 | 136 dist-ord : {p q r : HOD } → (p ∩ ( q ∪ r )) =h= ( ( p ∩ q ) ∪ ( p ∩ r )) |
| 137 dist-ord {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 } where | |
| 431 | 138 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x |
| 139 lemma1 {x} lt with proj2 lt | |
| 1465 | 140 lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ |
| 141 lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ | |
| 431 | 142 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x |
| 1465 | 143 lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ |
| 144 lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ | |
| 431 | 145 |
| 1464 | 146 dist-ord2 : {p q r : HOD } → (p ∪ ( q ∩ r )) =h= ( ( p ∪ q ) ∩ ( p ∪ r )) |
| 147 dist-ord2 {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 } where | |
| 431 | 148 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x |
| 149 lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫ | |
| 150 lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫ | |
| 151 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x | |
| 152 lemma2 {x} lt with proj1 lt | proj2 lt | |
| 153 lemma2 {x} lt | case1 cp | _ = case1 cp | |
| 1465 | 154 lemma2 {x} lt | _ | case1 cp = case1 cp |
| 155 lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ | |
| 431 | 156 |
| 1464 | 157 record IsBooleanAlgebra {n m : Level} ( L : Set n) |
| 1465 | 158 ( _≈_ : L → L → Set m ) |
| 431 | 159 ( b1 : L ) |
| 160 ( b0 : L ) | |
| 161 ( -_ : L → L ) | |
| 162 ( _+_ : L → L → L ) | |
| 1464 | 163 ( _x_ : L → L → L ) : Set (n ⊔ m) where |
| 431 | 164 field |
| 1465 | 165 +-assoc : {a b c : L } → (a + ( b + c )) ≈ ((a + b) + c) |
| 166 x-assoc : {a b c : L } → (a x ( b x c )) ≈ ((a x b) x c) | |
| 167 +-sym : {a b : L } → (a + b) ≈ (b + a) | |
| 168 x-sym : {a b : L } → (a x b) ≈ (b x a) | |
| 169 +-aab : {a b : L } → (a + ( a x b )) ≈ a | |
| 170 x-aab : {a b : L } → (a x ( a + b )) ≈ a | |
| 171 +-dist : {a b c : L } → (a + ( b x c )) ≈ (( a + b ) x ( a + c )) | |
| 172 x-dist : {a b c : L } → (a x ( b + c )) ≈ (( a x b ) + ( a x c )) | |
| 173 a+0 : {a : L } → (a + b0) ≈ a | |
| 174 ax1 : {a : L } → (a x b1) ≈ a | |
| 175 a+-a1 : {a : L } → (a + ( - a )) ≈ b1 | |
| 176 ax-a0 : {a : L } → (a x ( - a )) ≈ b0 | |
| 431 | 177 |
| 1464 | 178 record BooleanAlgebra {n m : Level} ( L : Set n) : Set (n ⊔ suc m) where |
| 431 | 179 field |
| 1465 | 180 _≈_ : L → L → Set m |
| 431 | 181 b1 : L |
| 182 b0 : L | |
| 1465 | 183 -_ : L → L |
| 431 | 184 _+_ : L → L → L |
| 185 _x_ : L → L → L | |
| 1465 | 186 isBooleanAlgebra : IsBooleanAlgebra L _≈_ b1 b0 -_ _+_ _x_ |
| 1280 | 187 |
| 188 record PowerP (P : HOD) : Set (suc n) where | |
| 189 constructor ⟦_,_⟧ | |
| 190 field | |
| 191 hod : HOD | |
| 1465 | 192 x⊆P : hod ⊆ P |
| 1280 | 193 |
| 194 open PowerP | |
| 195 | |
| 1464 | 196 HODBA : (P : HOD) → BooleanAlgebra {suc n} {n} (PowerP P) |
| 1465 | 197 HODBA P = record { _≈_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧ ; b0 = ⟦ od∅ , (λ x → ⊥-elim (¬x<0 x)) ⟧ |
| 1280 | 198 ; -_ = λ x → ⟦ P ＼ hod x , proj1 ⟧ |
| 1465 | 199 ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt)) ⟧ |
| 1280 | 200 ; isBooleanAlgebra = record { |
| 1464 | 201 +-assoc = λ {a} {b} {c} → record { eq→ = ba01 a b c ; eq← = ba02 a b c } |
| 1465 | 202 ; x-assoc = λ {a} {b} {c} → |
| 203 record { eq→ = λ lt → ⟪ ⟪ proj1 lt , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt) ⟫ | |
| 204 ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt) , proj2 lt ⟫ ⟫ } | |
| 1464 | 205 ; +-sym = λ {a} {b} → record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt ; eq← = ba05 {hod b} {hod a} } |
| 206 ; x-sym = λ {a} {b} → record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫ } | |
| 207 ; +-aab = λ {a} {b} → record { eq→ = ba03 a b ; eq← = case1 } | |
| 208 ; x-aab = λ {a} {b} → record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , case1 ax ⟫ } | |
| 1465 | 209 ; +-dist = λ {p} {q} {r} → dist-ord2 {hod p} {hod q} {hod r} |
| 210 ; x-dist = λ {p} {q} {r} → dist-ord {hod p} {hod q} {hod r} | |
| 1464 | 211 ; a+0 = λ {a} → record { eq→ = ba04 (hod a) ; eq← = case1 } |
| 212 ; ax1 = λ {a} → record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ } | |
| 213 ; a+-a1 = λ {a} → record { eq→ = ba06 a ; eq← = ba07 a } | |
| 214 ; ax-a0 = λ {a} → record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) } | |
| 1281 | 215 } } where |
| 216 ba00 : (x y : PowerP P ) → (hod x ∪ hod y) ⊆ P | |
| 217 ba00 x y (case1 px) = x⊆P x px | |
| 218 ba00 x y (case2 py) = x⊆P y py | |
| 219 ba01 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a) x ∨ odef (hod b ∪ hod c) x → | |
| 220 odef (hod a ∪ hod b) x ∨ odef (hod c) x | |
| 221 ba01 a b c {x} (case1 ax) = case1 (case1 ax) | |
| 222 ba01 a b c {x} (case2 (case1 bx)) = case1 (case2 bx) | |
| 223 ba01 a b c {x} (case2 (case2 cx)) = case2 cx | |
| 224 ba02 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a ∪ hod b) x ∨ odef (hod c) x | |
| 1465 | 225 → odef (hod a) x ∨ odef (hod b ∪ hod c) x |
| 1281 | 226 ba02 a b c {x} (case1 (case1 ax)) = case1 ax |
| 227 ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx) | |
| 228 ba02 a b c {x} (case2 cx) = case2 (case2 cx) | |
| 229 ba03 : (a b : PowerP P) → {x : Ordinal} → | |
| 1464 | 230 odef (hod a) x ∨ odef (hod a ∩ hod b) x → def (od (hod a)) x |
| 1281 | 231 ba03 a b (case1 ax) = ax |
| 232 ba03 a b (case2 ab) = proj1 ab | |
| 233 ba04 : (a : HOD) → {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x | |
| 234 ba04 a (case1 ax) = ax | |
| 235 ba04 a (case2 x) = ⊥-elim (¬x<0 x) | |
| 1282 | 236 ba05 : {a b : HOD} {x : Ordinal} → odef a x ∨ odef b x → odef b x ∨ odef a x |
| 237 ba05 (case1 x) = case2 x | |
| 238 ba05 (case2 x) = case1 x | |
| 1464 | 239 ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → def (od P) x |
| 1282 | 240 ba06 a {x} (case1 ax) = x⊆P a ax |
| 241 ba06 a {x} (case2 nax) = proj1 nax | |
| 1465 | 242 ba07 : (a : PowerP P ) → { x : Ordinal} → def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x |
| 1464 | 243 ba07 a {x} px with ODC.∋-p O HODAxiom AC (hod a) (* x) |
| 1282 | 244 ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y) |
| 245 ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫ | |
| 1464 | 246 ba08 : (a : PowerP P) → {x : Ordinal} → def (od (hod a ∩ (P ＼ hod a))) x → def (od od∅) x |
| 1282 | 247 ba08 a {x} ⟪ ax , ⟪ px , nax ⟫ ⟫ = ⊥-elim ( nax ax ) |
| 248 |