If the conversion c1 returns |- t = t' when applied to a term `t`, and
c2 returns |- t' = t'' when applied to `t'`, then the composite
conversion (c1 THENC c2) `t` returns |- t = t''. That is, (c1 THENC c2)
`t` has the effect of transforming the term `t` first with the conversion
c1 and then with the conversion c2.
FAILURE CONDITIONS
(c1 THENC c2) `t` fails if either the conversion c1 fails when applied to
`t`, or if c1 `t` succeeds and returns |- t = t' but c2 fails when
applied to `t'`. (c1 THENC c2) `t` may also fail if either of c1 or c2
is not, in fact, a conversion (i.e. a function that maps a term t to a
theorem |- t = t').
EXAMPLE
# BETA_CONV `(\x. x + 1) 3`;;
val it : thm = |- (\x. x + 1) 3 = 3 + 1
# (BETA_CONV THENC NUM_ADD_CONV) `(\x. x + 1) 3`;;
val it : thm = |- (\x. x + 1) 3 = 4