lets
+ let <hidden>
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` ref <hidden>
|   ` <*>
|     + <*>
|     | + <*>
|     | | + pure (\u1 -> (\u2 -> u1))
|     | | ` pure (\u1 -> u1)
|     | ` <*>
|     |   + <*>
|     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |   | ` pure Term
|     |   ` ref <hidden>
|     ` pure Term
+ let <hidden>
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` ref <hidden>
|   ` <*>
|     + <*>
|     | + <*>
|     | | + pure (\u1 -> (\u2 -> u1))
|     | | ` pure (\u1 -> u1)
|     | ` <*>
|     |   + <*>
|     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |   | ` ref <hidden>
|     |   ` ref <hidden>
|     ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + <*>
|   |   | | + pure (\u1 -> (\u2 -> u1))
|   |   | | ` pure (\u1 -> u1)
|   |   | ` <*>
|   |   |   + <*>
|   |   |   | + pure (\u1 -> (\u2 -> u1))
|   |   |   | ` <*>
|   |   |   |   + <*>
|   |   |   |   | + pure (\u1 -> (\u2 -> u1))
|   |   |   |   | ` pure '['
|   |   |   |   ` satisfy
|   |   |   ` ref <hidden>
|   |   ` <*>
|   |     + <*>
|   |     | + <*>
|   |     | | + pure (\u1 -> (\u2 -> u1))
|   |     | | ` pure (\u1 -> u1)
|   |     | ` ref <hidden>
|   |     ` <*>
|   |       + <*>
|   |       | + <*>
|   |       | | + pure (\u1 -> (\u2 -> u1))
|   |       | | ` pure (\u1 -> u1)
|   |       | ` <*>
|   |       |   + <*>
|   |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |       |   | ` pure Term
|   |       |   ` ref <hidden>
|   |       ` pure Term
|   ` <*>
|     + <*>
|     | + pure (\u1 -> (\u2 -> u1))
|     | ` <*>
|     |   + <*>
|     |   | + pure (\u1 -> (\u2 -> u1))
|     |   | ` pure ']'
|     |   ` satisfy
|     ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + <*>
|   |   | | + pure (\u1 -> (\u2 -> u1))
|   |   | | ` pure (\u1 -> u1)
|   |   | ` <*>
|   |   |   + <*>
|   |   |   | + pure (\u1 -> (\u2 -> u1))
|   |   |   | ` <*>
|   |   |   |   + <*>
|   |   |   |   | + pure (\u1 -> (\u2 -> u1))
|   |   |   |   | ` pure '{'
|   |   |   |   ` satisfy
|   |   |   ` ref <hidden>
|   |   ` <*>
|   |     + <*>
|   |     | + <*>
|   |     | | + pure (\u1 -> (\u2 -> u1))
|   |     | | ` pure (\u1 -> u1)
|   |     | ` <*>
|   |     |   + <*>
|   |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |     |   | ` ref <hidden>
|   |     |   ` ref <hidden>
|   |     ` ref <hidden>
|   ` <*>
|     + <*>
|     | + pure (\u1 -> (\u2 -> u1))
|     | ` <*>
|     |   + <*>
|     |   | + pure (\u1 -> (\u2 -> u1))
|     |   | ` pure '}'
|     |   ` satisfy
|     ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` ref <hidden>
|   ` <|>
|     + <*>
|     | + <*>
|     | | + pure (\u1 -> (\u2 -> u1))
|     | | ` pure Term
|     | ` ref <hidden>
|     ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` satisfy
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` try
|   |   ` <*>
|   |     + <*>
|   |     | + <*>
|   |     | | + pure (\u1 -> (\u2 -> u1))
|   |     | | ` pure (\u1 -> u1)
|   |     | ` satisfy
|   |     ` <*>
|   |       + <*>
|   |       | + <*>
|   |       | | + pure (\u1 -> (\u2 -> u1))
|   |       | | ` pure (\u1 -> u1)
|   |       | ` <*>
|   |       |   + <*>
|   |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |       |   | ` ref <hidden>
|   |       |   ` ref <hidden>
|   |       ` ref <hidden>
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + pure (\u1 -> (\u2 -> u1))
|   |   | ` pure '('
|   |   ` satisfy
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + pure (\u1 -> (\u2 -> u1))
|   |   | ` pure ')'
|   |   ` satisfy
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + pure (\u1 -> (\u2 -> u1))
|   |   | ` pure ','
|   |   ` satisfy
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + <*>
|   | + pure (\u1 -> (\u2 -> u1))
|   | ` <*>
|   |   + <*>
|   |   | + pure (\u1 -> (\u2 -> u1))
|   |   | ` pure ';'
|   |   ` satisfy
|   ` ref <hidden>
+ let <hidden>
| ` <*>
|   + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   ` pure (\u1 -> (\u2 -> u1))
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` <*>
|   | |     |   + <*>
|   | |     |   | + <*>
|   | |     |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |   | | ` pure (\u1 -> u1)
|   | |     |   | ` <*>
|   | |     |   |   + <*>
|   | |     |   |   | + <*>
|   | |     |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   | | ` pure (\u1 -> u1)
|   | |     |   |   | ` <*>
|   | |     |   |   |   + <*>
|   | |     |   |   |   | + <*>
|   | |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   | | ` pure (\u1 -> u1)
|   | |     |   |   |   | ` try
|   | |     |   |   |   |   ` <*>
|   | |     |   |   |   |     + <*>
|   | |     |   |   |   |     | + pure cons
|   | |     |   |   |   |     | ` <*>
|   | |     |   |   |   |     |   + <*>
|   | |     |   |   |   |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |     |   | ` pure 'f'
|   | |     |   |   |   |     |   ` satisfy
|   | |     |   |   |   |     ` <*>
|   | |     |   |   |   |       + <*>
|   | |     |   |   |   |       | + pure cons
|   | |     |   |   |   |       | ` <*>
|   | |     |   |   |   |       |   + <*>
|   | |     |   |   |   |       |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |       |   | ` pure 'u'
|   | |     |   |   |   |       |   ` satisfy
|   | |     |   |   |   |       ` <*>
|   | |     |   |   |   |         + <*>
|   | |     |   |   |   |         | + pure cons
|   | |     |   |   |   |         | ` <*>
|   | |     |   |   |   |         |   + <*>
|   | |     |   |   |   |         |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |         |   | ` pure 'n'
|   | |     |   |   |   |         |   ` satisfy
|   | |     |   |   |   |         ` <*>
|   | |     |   |   |   |           + <*>
|   | |     |   |   |   |           | + pure cons
|   | |     |   |   |   |           | ` <*>
|   | |     |   |   |   |           |   + <*>
|   | |     |   |   |   |           |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |           |   | ` pure 'c'
|   | |     |   |   |   |           |   ` satisfy
|   | |     |   |   |   |           ` <*>
|   | |     |   |   |   |             + <*>
|   | |     |   |   |   |             | + pure cons
|   | |     |   |   |   |             | ` <*>
|   | |     |   |   |   |             |   + <*>
|   | |     |   |   |   |             |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |             |   | ` pure 't'
|   | |     |   |   |   |             |   ` satisfy
|   | |     |   |   |   |             ` <*>
|   | |     |   |   |   |               + <*>
|   | |     |   |   |   |               | + pure cons
|   | |     |   |   |   |               | ` <*>
|   | |     |   |   |   |               |   + <*>
|   | |     |   |   |   |               |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |               |   | ` pure 'i'
|   | |     |   |   |   |               |   ` satisfy
|   | |     |   |   |   |               ` <*>
|   | |     |   |   |   |                 + <*>
|   | |     |   |   |   |                 | + pure cons
|   | |     |   |   |   |                 | ` <*>
|   | |     |   |   |   |                 |   + <*>
|   | |     |   |   |   |                 |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |                 |   | ` pure 'o'
|   | |     |   |   |   |                 |   ` satisfy
|   | |     |   |   |   |                 ` <*>
|   | |     |   |   |   |                   + <*>
|   | |     |   |   |   |                   | + pure cons
|   | |     |   |   |   |                   | ` <*>
|   | |     |   |   |   |                   |   + <*>
|   | |     |   |   |   |                   |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   |   |                   |   | ` pure 'n'
|   | |     |   |   |   |                   |   ` satisfy
|   | |     |   |   |   |                   ` pure Term
|   | |     |   |   |   ` ref <hidden>
|   | |     |   |   ` ref <hidden>
|   | |     |   ` <*>
|   | |     |     + <*>
|   | |     |     | + pure (\u1 -> (\u2 -> u1))
|   | |     |     | ` <*>
|   | |     |     |   + <*>
|   | |     |     |   | + <*>
|   | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   | | ` pure (\u1 -> u1)
|   | |     |     |   | ` ref <hidden>
|   | |     |     |   ` <*>
|   | |     |     |     + <*>
|   | |     |     |     | + <*>
|   | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |     | | ` pure (\u1 -> u1)
|   | |     |     |     | ` ref <hidden>
|   | |     |     |     ` <|>
|   | |     |     |       + <*>
|   | |     |     |       | + <*>
|   | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |       | | ` pure Term
|   | |     |     |       | ` <*>
|   | |     |     |       |   + <*>
|   | |     |     |       |   | + <*>
|   | |     |     |       |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |       |   | | ` pure (\u1 -> u1)
|   | |     |     |       |   | ` <*>
|   | |     |     |       |   |   + <*>
|   | |     |     |       |   |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |       |   |   | ` <*>
|   | |     |     |       |   |   |   + <*>
|   | |     |     |       |   |   |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |       |   |   |   | ` pure ':'
|   | |     |     |       |   |   |   ` satisfy
|   | |     |     |       |   |   ` ref <hidden>
|   | |     |     |       |   ` ref <hidden>
|   | |     |     |       ` ref <hidden>
|   | |     |     ` ref <hidden>
|   | |     ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` <*>
|   | |     |   + <*>
|   | |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   | ` <*>
|   | |     |   |   + <*>
|   | |     |   |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |   |   | ` pure '!'
|   | |     |   |   ` satisfy
|   | |     |   ` ref <hidden>
|   | |     ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` <|>
|   | |     + <|>
|   | |     | + <|>
|   | |     | | + <*>
|   | |     | | | + <*>
|   | |     | | | | + <*>
|   | |     | | | | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | | | | ` pure (\u1 -> u1)
|   | |     | | | | ` try
|   | |     | | | |   ` <*>
|   | |     | | | |     + <*>
|   | |     | | | |     | + pure cons
|   | |     | | | |     | ` <*>
|   | |     | | | |     |   + <*>
|   | |     | | | |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | | | |     |   | ` pure 'i'
|   | |     | | | |     |   ` satisfy
|   | |     | | | |     ` <*>
|   | |     | | | |       + <*>
|   | |     | | | |       | + pure cons
|   | |     | | | |       | ` <*>
|   | |     | | | |       |   + <*>
|   | |     | | | |       |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | | | |       |   | ` pure 'f'
|   | |     | | | |       |   ` satisfy
|   | |     | | | |       ` pure Term
|   | |     | | | ` ref <hidden>
|   | |     | | ` <*>
|   | |     | |   + <*>
|   | |     | |   | + <*>
|   | |     | |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   | | ` pure (\u1 -> u1)
|   | |     | |   | ` <*>
|   | |     | |   |   + <*>
|   | |     | |   |   | + <*>
|   | |     | |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   | | ` pure (\u1 -> u1)
|   | |     | |   |   | ` <*>
|   | |     | |   |   |   + <*>
|   | |     | |   |   |   | + <*>
|   | |     | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   | | ` pure (\u1 -> u1)
|   | |     | |   |   |   | ` try
|   | |     | |   |   |   |   ` <*>
|   | |     | |   |   |   |     + <*>
|   | |     | |   |   |   |     | + pure cons
|   | |     | |   |   |   |     | ` <*>
|   | |     | |   |   |   |     |   + <*>
|   | |     | |   |   |   |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   |     |   | ` pure 'w'
|   | |     | |   |   |   |     |   ` satisfy
|   | |     | |   |   |   |     ` <*>
|   | |     | |   |   |   |       + <*>
|   | |     | |   |   |   |       | + pure cons
|   | |     | |   |   |   |       | ` <*>
|   | |     | |   |   |   |       |   + <*>
|   | |     | |   |   |   |       |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   |       |   | ` pure 'h'
|   | |     | |   |   |   |       |   ` satisfy
|   | |     | |   |   |   |       ` <*>
|   | |     | |   |   |   |         + <*>
|   | |     | |   |   |   |         | + pure cons
|   | |     | |   |   |   |         | ` <*>
|   | |     | |   |   |   |         |   + <*>
|   | |     | |   |   |   |         |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   |         |   | ` pure 'i'
|   | |     | |   |   |   |         |   ` satisfy
|   | |     | |   |   |   |         ` <*>
|   | |     | |   |   |   |           + <*>
|   | |     | |   |   |   |           | + pure cons
|   | |     | |   |   |   |           | ` <*>
|   | |     | |   |   |   |           |   + <*>
|   | |     | |   |   |   |           |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   |           |   | ` pure 'l'
|   | |     | |   |   |   |           |   ` satisfy
|   | |     | |   |   |   |           ` <*>
|   | |     | |   |   |   |             + <*>
|   | |     | |   |   |   |             | + pure cons
|   | |     | |   |   |   |             | ` <*>
|   | |     | |   |   |   |             |   + <*>
|   | |     | |   |   |   |             |   | + pure (\u1 -> (\u2 -> u1))
|   | |     | |   |   |   |             |   | ` pure 'e'
|   | |     | |   |   |   |             |   ` satisfy
|   | |     | |   |   |   |             ` pure Term
|   | |     | |   |   |   ` ref <hidden>
|   | |     | |   |   ` ref <hidden>
|   | |     | |   ` rec <hidden>
|   | |     | ` try
|   | |     |   ` <*>
|   | |     |     + <*>
|   | |     |     | + pure (\u1 -> (\u2 -> u1))
|   | |     |     | ` <*>
|   | |     |     |   + <*>
|   | |     |     |   | + <*>
|   | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   | | ` pure (\u1 -> u1)
|   | |     |     |   | ` <*>
|   | |     |     |   |   + <*>
|   | |     |     |   |   | + <*>
|   | |     |     |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   | | ` pure (\u1 -> u1)
|   | |     |     |   |   | ` <*>
|   | |     |     |   |   |   + <*>
|   | |     |     |   |   |   | + <*>
|   | |     |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   | | ` pure (\u1 -> u1)
|   | |     |     |   |   |   | ` <|>
|   | |     |     |   |   |   |   + <*>
|   | |     |     |   |   |   |   | + <*>
|   | |     |     |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   |   | | ` pure Term
|   | |     |     |   |   |   |   | ` <*>
|   | |     |     |   |   |   |   |   + <*>
|   | |     |     |   |   |   |   |   | + <*>
|   | |     |     |   |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   |   |   | | ` pure (\u1 -> u1)
|   | |     |     |   |   |   |   |   | ` try
|   | |     |     |   |   |   |   |   |   ` <*>
|   | |     |     |   |   |   |   |   |     + <*>
|   | |     |     |   |   |   |   |   |     | + pure cons
|   | |     |     |   |   |   |   |   |     | ` <*>
|   | |     |     |   |   |   |   |   |     |   + <*>
|   | |     |     |   |   |   |   |   |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   |   |   |     |   | ` pure 'v'
|   | |     |     |   |   |   |   |   |     |   ` satisfy
|   | |     |     |   |   |   |   |   |     ` <*>
|   | |     |     |   |   |   |   |   |       + <*>
|   | |     |     |   |   |   |   |   |       | + pure cons
|   | |     |     |   |   |   |   |   |       | ` <*>
|   | |     |     |   |   |   |   |   |       |   + <*>
|   | |     |     |   |   |   |   |   |       |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   |   |   |       |   | ` pure 'a'
|   | |     |     |   |   |   |   |   |       |   ` satisfy
|   | |     |     |   |   |   |   |   |       ` <*>
|   | |     |     |   |   |   |   |   |         + <*>
|   | |     |     |   |   |   |   |   |         | + pure cons
|   | |     |     |   |   |   |   |   |         | ` <*>
|   | |     |     |   |   |   |   |   |         |   + <*>
|   | |     |     |   |   |   |   |   |         |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |   |   |   |         |   | ` pure 'r'
|   | |     |     |   |   |   |   |   |         |   ` satisfy
|   | |     |     |   |   |   |   |   |         ` pure Term
|   | |     |     |   |   |   |   |   ` ref <hidden>
|   | |     |     |   |   |   |   ` ref <hidden>
|   | |     |     |   |   |   ` <*>
|   | |     |     |   |   |     + <*>
|   | |     |     |   |   |     | + <*>
|   | |     |     |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |     | | ` pure (\u1 -> u1)
|   | |     |     |   |   |     | ` ref <hidden>
|   | |     |     |   |   |     ` <*>
|   | |     |     |   |   |       + <*>
|   | |     |     |   |   |       | + <*>
|   | |     |     |   |   |       | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |   |       | | ` pure (\u1 -> u1)
|   | |     |     |   |   |       | ` <*>
|   | |     |     |   |   |       |   + <*>
|   | |     |     |   |   |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   | |     |     |   |   |       |   | ` ref <hidden>
|   | |     |     |   |   |       |   ` ref <hidden>
|   | |     |     |   |   |       ` ref <hidden>
|   | |     |     |   |   ` <*>
|   | |     |     |   |     + <*>
|   | |     |     |   |     | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |     | ` <*>
|   | |     |     |   |     |   + <*>
|   | |     |     |   |     |   | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |   |     |   | ` pure '='
|   | |     |     |   |     |   ` satisfy
|   | |     |     |   |     ` ref <hidden>
|   | |     |     |   ` <*>
|   | |     |     |     + <*>
|   | |     |     |     | + <*>
|   | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |     | | ` pure (\u1 -> u1)
|   | |     |     |     | ` ref <hidden>
|   | |     |     |     ` <*>
|   | |     |     |       + <*>
|   | |     |     |       | + <*>
|   | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
|   | |     |     |       | | ` pure (\u1 -> u1)
|   | |     |     |       | ` <*>
|   | |     |     |       |   + <*>
|   | |     |     |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   | |     |     |       |   | ` ref <hidden>
|   | |     |     |       |   ` ref <hidden>
|   | |     |     |       ` ref <hidden>
|   | |     |     ` ref <hidden>
|   | |     ` <*>
|   | |       + <*>
|   | |       | + pure (\u1 -> (\u2 -> u1))
|   | |       | ` ref <hidden>
|   | |       ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + <*>
|   | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   | |   | ` pure (\u1 -> (\u2 -> u1))
|   | |   ` satisfy
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + ref <hidden>
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` ref <hidden>
|   | |     ` rec <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + ref <hidden>
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` ref <hidden>
|   | |     ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + ref <hidden>
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` ref <hidden>
|   | |     ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   | | ` <*>
|   | |   + ref <hidden>
|   | |   ` <*>
|   | |     + <*>
|   | |     | + <*>
|   | |     | | + pure (\u1 -> (\u2 -> u1))
|   | |     | | ` pure (\u1 -> u1)
|   | |     | ` ref <hidden>
|   | |     ` ref <hidden>
|   | ` rec <hidden>
|   ` pure (\u1 -> u1)
+ let <hidden>
| ` <|>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure Term
|   | ` <*>
|   |   + <*>
|   |   | + <*>
|   |   | | + pure (\u1 -> (\u2 -> u1))
|   |   | | ` pure (\u1 -> u1)
|   |   | ` ref <hidden>
|   |   ` <*>
|   |     + <*>
|   |     | + <*>
|   |     | | + pure (\u1 -> (\u2 -> u1))
|   |     | | ` pure (\u1 -> u1)
|   |     | ` <*>
|   |     |   + <*>
|   |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |     |   | ` ref <hidden>
|   |     |   ` ref <hidden>
|   |     ` ref <hidden>
|   ` ref <hidden>
+ let <hidden>
| ` <|>
|   + <|>
|   | + <*>
|   | | + <*>
|   | | | + <*>
|   | | | | + pure (\u1 -> (\u2 -> u1))
|   | | | | ` pure (\u1 -> u1)
|   | | | ` <|>
|   | | |   + <*>
|   | | |   | + <*>
|   | | |   | | + pure (\u1 -> (\u2 -> u1))
|   | | |   | | ` pure '0'
|   | | |   | ` satisfy
|   | | |   ` <*>
|   | | |     + <*>
|   | | |     | + pure (\u1 -> (\u2 -> u1))
|   | | |     | ` pure '1'
|   | | |     ` satisfy
|   | | ` ref <hidden>
|   | ` <*>
|   |   + <*>
|   |   | + pure (\u1 -> (\u2 -> u1))
|   |   | ` <*>
|   |   |   + <*>
|   |   |   | + <*>
|   |   |   | | + pure (\u1 -> (\u2 -> u1))
|   |   |   | | ` pure (\u1 -> u1)
|   |   |   | ` <*>
|   |   |   |   + <*>
|   |   |   |   | + pure (\u1 -> (\u2 -> u1))
|   |   |   |   | ` pure '\''
|   |   |   |   ` satisfy
|   |   |   ` <|>
|   |   |     + <*>
|   |   |     | + <*>
|   |   |     | | + <*>
|   |   |     | | | + pure (\u1 -> (\u2 -> u1))
|   |   |     | | | ` pure (\u1 -> u1)
|   |   |     | | ` satisfy
|   |   |     | ` ref <hidden>
|   |   |     ` <*>
|   |   |       + <*>
|   |   |       | + <*>
|   |   |       | | + pure (\u1 -> (\u2 -> u1))
|   |   |       | | ` pure (\u1 -> u1)
|   |   |       | ` <*>
|   |   |       |   + <*>
|   |   |       |   | + pure (\u1 -> (\u2 -> u1))
|   |   |       |   | ` pure '\\'
|   |   |       |   ` satisfy
|   |   |       ` <*>
|   |   |         + <*>
|   |   |         | + <*>
|   |   |         | | + pure (\u1 -> (\u2 -> u1))
|   |   |         | | ` pure (\u1 -> u1)
|   |   |         | ` satisfy
|   |   |         ` ref <hidden>
|   |   ` <*>
|   |     + <*>
|   |     | + pure (\u1 -> (\u2 -> u1))
|   |     | ` <*>
|   |     |   + <*>
|   |     |   | + pure (\u1 -> (\u2 -> u1))
|   |     |   | ` pure '\''
|   |     |   ` satisfy
|   |     ` ref <hidden>
|   ` <*>
|     + <*>
|     | + <*>
|     | | + pure (\u1 -> (\u2 -> u1))
|     | | ` pure (\u1 -> u1)
|     | ` ref <hidden>
|     ` <|>
|       + <*>
|       | + <*>
|       | | + pure (\u1 -> (\u2 -> u1))
|       | | ` pure Term
|       | ` <|>
|       |   + <*>
|       |   | + <*>
|       |   | | + pure (\u1 -> (\u2 -> u1))
|       |   | | ` <*>
|       |   | |   + <*>
|       |   | |   | + <*>
|       |   | |   | | + pure (\u1 -> (\u2 -> u1))
|       |   | |   | | ` pure (\u1 -> u1)
|       |   | |   | ` ref <hidden>
|       |   | |   ` <|>
|       |   | |     + <*>
|       |   | |     | + <*>
|       |   | |     | | + pure (\u1 -> (\u2 -> u1))
|       |   | |     | | ` pure Term
|       |   | |     | ` <*>
|       |   | |     |   + <*>
|       |   | |     |   | + <*>
|       |   | |     |   | | + pure (\u1 -> (\u2 -> u1))
|       |   | |     |   | | ` pure (\u1 -> u1)
|       |   | |     |   | ` rec <hidden>
|       |   | |     |   ` <*>
|       |   | |     |     + <*>
|       |   | |     |     | + <*>
|       |   | |     |     | | + pure (\u1 -> (\u2 -> u1))
|       |   | |     |     | | ` pure (\u1 -> u1)
|       |   | |     |     | ` <*>
|       |   | |     |     |   + <*>
|       |   | |     |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|       |   | |     |     |   | ` ref <hidden>
|       |   | |     |     |   ` ref <hidden>
|       |   | |     |     ` ref <hidden>
|       |   | |     ` ref <hidden>
|       |   | ` ref <hidden>
|       |   ` ref <hidden>
|       ` ref <hidden>
+ let <hidden>
| ` pure Term
+ let <hidden>
| ` pure Term
+ let <hidden>
| ` satisfy
` <*>
  + pure Term
  ` <*>
    + <*>
    | + pure (\u1 -> (\u2 -> u1))
    | ` <*>
    |   + <*>
    |   | + <*>
    |   | | + pure (\u1 -> (\u2 -> u1))
    |   | | ` pure (\u1 -> u1)
    |   | ` ref <hidden>
    |   ` <*>
    |     + <*>
    |     | + <*>
    |     | | + pure (\u1 -> (\u2 -> u1))
    |     | | ` pure (\u1 -> u1)
    |     | ` <*>
    |     |   + <*>
    |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
    |     |   | ` ref <hidden>
    |     |   ` ref <hidden>
    |     ` ref <hidden>
    ` eof