PAT_CONV : term -> conv -> conv
# PAT_CONV `\x. x + a + x` NUM_ADD_CONV `(1 + 2) + (3 + 4) + (5 + 6)`;; val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = 3 + (3 + 4) + 11
# PAT_CONV `\x. !x1 x2 x3 x4 x5. x` (REWR_CONV SWAP_FORALL_THM) `!a b c d e f g h. something`;; Warning: inventing type variables Warning: inventing type variables val it : thm = |- (!a b c d e f g h. something) <=> (!a b c d e g f h. something)