sig
  val first :
    ProofEngine.tree ->
    anchor:ProofEngine.node -> Strategy.t array -> ProofEngine.fork option
  val backtrack :
    ProofEngine.tree ->
    anchor:ProofEngine.node -> loop:bool -> ProofEngine.fork option
end