(define super
  {(progression A) --> (A --> B) --> (B --> (lazy C) --> C) --> C --> C}
    [B S T] P F Y -> (if (T B) 
                         Y 
                         (F (P B) (freeze (super [(S B) S T] P F Y)))))
                         
(define and'
   {boolean --> (lazy boolean) --> boolean}
    false _ -> false
    _ Lazy -> (thaw Lazy))
   
(define or'
   {boolean --> (lazy boolean) --> boolean}
    true _ -> true
    _ Lazy -> (thaw Lazy))

(define show
  {string --> A --> boolean}
  String X -> (do (output "~A ~S~%" String X) true))

(define forall
  {(progression A) --> (A --> boolean) --> boolean}
  Progression P -> (super Progression P (fn and') true)) 
 
(define exists
  {(progression A) --> (A --> boolean) --> boolean}
  Progression P -> (super Progression P (fn or') false))   	  


\\ (exists M [1 (+ 1) (= 100)]  (exists N [10 (+ 1) (= 100)]
  \\              (((integer? (N / 9)) & (N = (M * M))) & (show "N =" N))))