Write conversion to lift constructors out of case expressions

[mn200]

Something like

  case v of (x, INL y) => C (f x y) | (a, INR b) => C (g a b)

can be simplified to

  C (case v of (x,INL y) => f x y | (a, INR b) => g a b)

by applying the appropriate TypeBase.case_rand_of theorems backwards. These theorems won't match unless specialised with the function being lifted out, and constructors are good candidates to be lifted out so that the various automatic theorems about them can apply. A conversion to do this generally would just be able to detect whether or not a term was a constructor.

Otherwise, for special cases, the user might specialise with “constructors” like $+ 10 or similar.

Thanks to @mktnk3 for discussion leading to this idea.