logtk
InnerTerm.Pos
logtk.parsers
logtk.proofs
val at : t -> Position.t -> t
retrieve subterm at pos, or raise Invalid_argument
val replace : t -> Position.t -> by:t -> t
replace t|_p by the second term