📥 Download raw
module Padova2025.ComputationalContent.Fictions.Drinkers (⊥ : Set) where

Drinkers

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ComputationalContent.DoubleNegation (⊥)

drinker : (f : ℕ → Bool) → ¬ ¬ (Σ[ n ∈ ℕ ] (f n ≡ true → ((m : ℕ) → ¬ ¬ (f m ≡ true))))
drinker = {!!}