val get_eqn : t -> Position.t -> (term * term * bool) optionView of a Prop or Equation literal, oriented by the position. If the position selects its left term, return l, r, otherwise r, l. for propositions it will always be p, true.
None for other literals
Invalid_argument if the position doesn't match the literal.
val focus_arith : t -> Position.t -> Int_lit.Focus.t optionFocus on a specific term in an arithmetic literal. The focused term is removed from its monome, and its coefficient is returned.
val unfocus_arith : Int_lit.Focus.t -> tval focus_rat : t -> Position.t -> Rat_lit.Focus.t optionFocus on a specific term in an arithmetic literal. The focused term is removed from its monome, and its coefficient is returned.
val unfocus_rat : Rat_lit.Focus.t -> t