# e(REPEAT STRIP_TAC THEN MAP_EVERY ABBREV_TAC
[`Y = {b:A->bool | f(b) SUBSET b}`; `a:A->bool = INTERS Y`] THEN
SUBGOAL_THEN `!b:A->bool. b IN Y <=> f(b) SUBSET b` ASSUME_TAC THENL
[EXPAND_TAC "Y" THEN REWRITE_TAC[IN_ELIM_THM]; ALL_TAC] THEN
SUBGOAL_THEN `!b:A->bool. b IN Y ==> f(a:A->bool) SUBSET b`
ASSUME_TAC THENL
[ASM_MESON_TAC[SUBSET_TRANS; IN_INTERS; SUBSET]; ALL_TAC]);;
...
val it : goalstack = 1 subgoal (1 total)
0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
1 [`{b | f b SUBSET b} = Y`]
2 [`INTERS Y = a`]
3 [`!b. b IN Y <=> f b SUBSET b`]
4 [`!b. b IN Y ==> f a SUBSET b`]
`?s. f s = s`
Now we select a particularly interesting lemma:
# e(SUBGOAL_THEN `f(a:A->bool) SUBSET a` ASSUME_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
1 [`{b | f b SUBSET b} = Y`]
2 [`INTERS Y = a`]
3 [`!b. b IN Y <=> f b SUBSET b`]
4 [`!b. b IN Y ==> f a SUBSET b`]
5 [`f a SUBSET a`]
`?s. f s = s`
0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
1 [`{b | f b SUBSET b} = Y`]
2 [`INTERS Y = a`]
3 [`!b. b IN Y <=> f b SUBSET b`]
4 [`!b. b IN Y ==> f a SUBSET b`]
`f a SUBSET a`
The lemma is relatively easy to prove by giving