1% Proof of Cantor's Theorem %
2
3let Th1 = ASSUME "!fn:*->bool. ?x:*. fn = FN x";;
4
5let Th2 = SPEC "\x. ~((FN:*->*->bool) x x)" Th1;;
6
7let Th3 = SELECT_RULE Th2;;
8
9let t = rand(rhs(concl Th3));;
10
11let Th4 = AP_THM Th3 t;;
12
13let Th5 = CONV_RULE(DEPTH_CONV BETA_CONV) Th4;;
14
15let Lemma1 =
16 TAC_PROOF
17  (([],"!t. (~t = t) = F"), 
18   GEN_TAC THEN BOOL_CASES_TAC "t:bool" THEN REWRITE_TAC[]);;
19
20let Th6 = REWRITE_RULE[Lemma1] Th5;;
21
22let Th7 =
23 CHOOSE ("FN:*->*->bool", ASSUME "?FN. !fn:*->bool. ?x:*. fn = FN x") Th6;;
24
25let Th8 = DISCH_ALL Th7;;
26
27let Cantors_Thm = NOT_INTRO Th8;;
28
29
30