`prove_cases_thm : thm -> thm`

SYNOPSIS
Proves a structural cases theorem for an automatically-defined concrete type.

DESCRIPTION
prove_cases_thm takes as its argument a structural induction theorem, in the form returned by prove_induction_thm for an automatically-defined concrete type. When applied to such a theorem, prove_cases_thm automatically proves and returns a theorem which states that every value the concrete type in question is denoted by the value returned by some constructor of the type.

FAILURE CONDITIONS
Fails if the argument is not a theorem of the form returned by prove_induction_thm

EXAMPLE
The following type definition for labelled binary trees:
```  # let ith,rth = define_type "tree = LEAF num | NODE tree tree";;
val ith : thm =
|- !P. (!a. P (LEAF a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (NODE a0 a1))
==> (!x. P x)
val rth : thm =
|- !f0 f1.
?fn. (!a. fn (LEAF a) = f0 a) /\
(!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1))
```
returns an induction theorem ith that can then be fed to prove_cases_thm:
```  # prove_cases_thm ith;;
val it : thm = |- !x. (?a. x = LEAF a) \/ (?a0 a1. x = NODE a0 a1)
```