let is_pure = Term.is_pure Th.cop