cond [a] {Infinite} :-
    [a] {a : [a] {Infinite}}

cond [a] {NonEmpty} :-
    [a] {a : [a]}

cond Maybe a {NonEmpty} :-
    Just a

newtype Stream a = Stream ([a] {Infinite})

data Finger a =
    One a
    Two a a
    Three a a a
    Four a a a a

newtype Node23 a = Node (Finger a {Two a a | Three a a a})