
f := λp . (
   (match p (
      ()
      ( () p )
      ( Nil p )
      ( (Variable _) p )
      ( (Literal _) p )
      ( (App( g x )) (
         (App( (f g) (f x) ))
      ))
      ( (Lambda( lhs rhs )) (
         (App( (f lhs) (f rhs) ))
      ))
      ( (prog (GExpr( g ))) (
         ( (f prog) (GExpr (f g)) )
      ))
      ( (prog (Global( n v ))) (
         ( (f prog) (Global( (f n) (f v) )) )
      ))
      ( (prog (Type( tn td ))) (
         ( (f prog) (Type( (f tn) (f td) )) )
      ))
      ( unknown (
         (UnknownTerm unknown)
      ))
   ))
);

main := print-s ( f (() (Global (S V))) );
