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