# e(DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "antisym") (LABEL_TAC "wo")));;
val it : goalstack = 1 subgoal (1 total)
0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
`(!x y. x <<= y \/ y <<= x) /\ (!x y z. x <<= y /\ y <<= z ==> x <<= z)`
Now we break down the goal a bit
# e(REPEAT STRIP_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
2 [`x <<= y`]
3 [`y <<= z`]
`x <<= z`
0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
`x <<= y \/ y <<= x`
We want to specialize the wellordering assumption to an appropriate
set for each case, and we can identify it using the label # e(USE_THEN "wo" (MP_TAC o SPEC `{x:A,y:A}`) THEN SET_TAC[]);;
...
val it : goalstack = 1 subgoal (1 total)
0 [`!x y. x <<= y /\ y <<= x ==> x = y`] (antisym)
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`] (wo)
2 [`x <<= y`]
3 [`y <<= z`]
`x <<= z`
Similarly for the other one:
# e(USE_THEN "wo" (MP_TAC o SPEC `{x:A,y:A,z:A}`) THEN ASM SET_TAC[]);;
...
val it : goalstack = No subgoals