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