let context_inv i = Context.inv (Th.of_int i)