let is_pure = Term.is_pure Th.p