`DISJ_CASES : thm -> thm -> thm -> thm`

SYNOPSIS
Eliminates disjunction by cases.

DESCRIPTION
The rule DISJ_CASES takes a disjunctive theorem, and two `case' theorems, each with one of the disjuncts as a hypothesis while sharing alpha-equivalent conclusions. A new theorem is returned with the same conclusion as the `case' theorems, and the union of all assumptions excepting the disjuncts.
```         A |- t1 \/ t2     A1 |- t      A2 |- t
--------------------------------------------------  DISJ_CASES
A u (A1 - {t1}) u (A2 - {t2}) |- t
```

FAILURE CONDITIONS
Fails if the first argument is not a disjunctive theorem, or if the conclusions of the other two theorems are not alpha-convertible.

EXAMPLE
Let us create several theorems. Note that th1 and th2 draw the same conclusion from different hypotheses, while th proves the disjunction of the two hypotheses:
```  # let [th; th1; th2] = map (UNDISCH_ALL o REAL_FIELD)
[`~(x = &0) \/ x = &0`;
`~(x = &0) ==> x * (inv(x) * x - &1) = &0`;
`x = &0 ==> x * (inv(x) * x - &1) = &0`];;
...
val th : thm = |- ~(x = &0) \/ x = &0
val th1 : thm = ~(x = &0) |- x * (inv x * x - &1) = &0
val th2 : thm = x = &0 |- x * (inv x * x - &1) = &0
```
so we can apply DISJ_CASES:
```  # DISJ_CASES th th1 th2;;
val it : thm = |- x * (inv x * x - &1) = &0
```