functor (T1 : TermInner.REPR) (T2 : TermInner.BUILD) ->
  sig
    type ('a, 'b, 'c) inv = < eqn : 'a; ind_preds : 'b; ty : 'c >
    val convert : (T1.t, T1.t) Problem.t -> (T2.t, T2.t) Problem.t
    val pipe :
      unit ->
      ((T1.t, T1.t) Problem.t, (T2.t, T2.t) Problem.t, 'ret, 'ret)
      Transform.t
  end