These were very specific, there were no lemmas about them. They were used
back in the days for some specific things in my C semantics.