\\ load 23.2 first

(datatype progression

E : A; S : (A --> A); T : (A --> boolean);
==========================================
[E S T] : (progression A);)

(define force
  {(progression A) --> A}
   [B _ _] -> B)

(define delay
   {(progression A) --> (progression A)}
    [B S T] -> [(S B) S T])
    
(define end?
   {(progression A) --> boolean}
   [B _ T] -> (T B))

(define unpack
   {(progression A) --> (list A)}
   [B S T] -> (if (T B) [] [B | (unpack (delay [B S T]))]))

(define exists
  {(progression A) --> (A --> boolean) --> boolean}
   Progression _ -> false	where (end? Progression)
   Progression P -> (or (P (force Progression)) (exists (delay Progression) P)))

(define forall
  {(progression A) --> (A --> boolean) --> boolean}
   Progression _ -> true	where (end? Progression)
   Progression P -> (and (P (force Progression)) (forall (delay Progression) P)))
   
(define next-prime
  {number --> number}
  N -> (let N+1 (+ N 1)
          (if (prime? N+1)
              N+1
              (next-prime N+1))))   

"
(exists X [1009 (fn next-prime) (/. X false)] (prime? (X + 2)))

(let Evens [4 (+ 2) (/. N false)]
      (forall X Evens 
        (let UpperBound (/. M (> M X))
              Primes [2 (fn next-prime) UpperBound]
              (exists Y Primes (exists Z Primes (X = (Y + Z)))))))
              "