Make defthm also enable undoing pseudo-infix, not just term.