Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ComputationalContent.Fictions.Drinkers (⊥ : Set) where

酒客（Drinkers）#

open import Padova2025-zh-TW.ProgrammingBasics.Booleans
open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.Equality.Base
open import Padova2025-zh-TW.ProvingBasics.Connectives.Existential
open import Padova2025-zh-TW.ComputationalContent.DoubleNegation (⊥)
習題 1drinker
drinker : (f : ℕ → Bool) → ¬ ¬ (Σ[ n ∈ ℕ ] (f n ≡ true → ((m : ℕ) → ¬ ¬ (f m ≡ true))))
drinker = {!!}
參考解答用到： zero _,_
參考解答
drinker : (f : ℕ → Bool) → ¬ ¬ (Σ[ n ∈ ℕ ] (f n ≡ true → ((m : ℕ) → ¬ ¬ (f m ≡ true))))
drinker f = λ k → k (zero , (λ f0≡true m fm≢true → k (m , (λ fm≡true m' fm'≢true → fm≢true fm≡true))))