-- BEGININFO -- TYPE|6|6 (nat → Prop) → nat -- ACK -- IDENTIFIER|6|6 epsilon -- ACK -- EXTRA_TYPE|6|14 λ (x : nat), true -- nat → Prop -- ACK -- SYMBOL|6|14 ( -- ACK -- SYMBOL|6|15 λ -- ACK -- TYPE|6|21 Type -- ACK -- IDENTIFIER|6|21 nat.nat -- ACK -- TYPE|6|26 Prop -- ACK -- IDENTIFIER|6|26 true -- ACK -- ENDINFO