Example (26)

　ある論文で紹介されていた排中律によるトリック？です．

# g `!p:A->bool. ?x:A. (p x ==> !y. p y)`;;
val it : goalstack = 1 subgoal (1 total)

`!p. ?x. p x ==> (!y. p y)`

# e(GEN_TAC);;
val it : goalstack = 1 subgoal (1 total)

`?x. p x ==> (!y. p y)`

# e(ASM_CASES_TAC `!y:A. (p:A->bool) y`);;
val it : goalstack = 2 subgoals (2 total)

  0 [`~(!y. p y)`]

`?x. p x ==> (!y. p y)`

  0 [`!y. p y`]

`?x. p x ==> (!y. p y)`

# e(ASM_SIMP_TAC[]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`~(!y. p y)`]

`?x. p x ==> (!y. p y)`

# e(POP_ASSUM MP_TAC THEN SIMP_TAC[NOT_FORALL_THM] THEN STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`~p y`]

`?x. p x ==> (!y. p y)`

# e(EXISTS_TAC`y:A`);;
val it : goalstack = 1 subgoal (1 total)

  0 [`~p y`]

`p y ==> (!y. p y)`

# e(ASM_SIMP_TAC[]);;
val it : goalstack = No subgoals