let pp fmt (a, b, rho) =   
    pp_justification fmt rho;
    Pretty.infix Term.pp " <> " Term.pp fmt (a, b)