You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
#lang quadwriter/markdown
|
|
|
|
```
|
|
excl-middl→¬¬-elim : ∀ {A : Set} → A ⊎ ¬ A → (¬ ¬ A → A)
|
|
excl-middl→¬¬-elim (inj₁ a) = λ ¬¬a → a
|
|
excl-middl→¬¬-elim (inj₂ ¬a) = λ ¬¬a → ⊥-elim (¬¬a ¬a)
|
|
```
|