Seemingly impossible functional program

Parth.ard

\import Data.Bool
\import Data.List
\import Logic.Meta
\import Paths

\func CoNat =>
  \Sigma (f : Nat -> Bool)
         (\Pi (i : _) -> f i = false -> f (suc i) = false)
  \where {
    \func blt (n m : Nat) : Bool
      | 0, suc m => true
      | suc n, suc m => blt n m
      | _, 0 => false

    \func ofNat (n : Nat) : CoNat => (blt __ n, lemma __ n) \where {
      \func lemma (m n : Nat) : blt m n = false -> blt (suc m) n = false
        | 0, 0 => \lam p => p
        | 0, suc n => contradiction
        | suc m, 0 => \lam p => p
        | suc m, suc n => lemma m n
    }

    \func inf : CoNat => (\lam _ => false, \lam _ x => x)

    \func preview (n : CoNat) : List Bool =>
      \let f => n.1 \in f 0 :: f 1 :: f 2 :: f 3 :: f 4 :: nil

    \func wtf => preview (ofNat 3)

    -- Checks if p i for i ≤ n is true
    -- if n is 0, then we only need to check p 0
    -- if n is suc n', recursively check for n' and make sure p n is true
    \func find' (p : CoNat -> Bool) (n : Nat) : Bool \elim n
      | 0 => p (ofNat 0)
      | suc n' \as n => find' p n' and p (ofNat n)

    \func find (p : CoNat -> Bool) : CoNat =>
      (find' p, \lam _ => pmap (__ and _))

    \func forall (p : CoNat -> Bool) : Bool => p (find p)
  }