1 push (\u1 -> (\u2 -> u1 : u2 Term))
5 | | push (\u1 -> (\u2 -> (\u3 -> (\u4 -> 'a' : ('b' : ('c' : ('d' : Term)))))))
7 | | lift (\u1 -> (\u2 -> u1 u2))
9 | | lift (\u1 -> (\u2 -> u1 u2))
11 | | lift (\u1 -> (\u2 -> u1 u2))
13 | | lift (\u1 -> (\u2 -> u1 u2))
20 lift (\u1 -> (\u2 -> u1 u2))
24 | | push (\u1 -> (\u2 -> (\u3 -> u1 : u2 u3)))
26 | | lift (\u1 -> (\u2 -> u1 u2))
28 | | lift (\u1 -> (\u2 -> u1 u2))
34 | choices [(\u1 -> u1)]
41 lift (\u1 -> (\u2 -> u1 u2))