``` nothing_with_counter#_ = ElemWithCounter 0 X; <- X here is marked with error elem_with_counter#_ {n:#} {X:Type} value:X = ElemWithCounter (n + 1) X; ```