equal
deleted
inserted
replaced
25 by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1); |
25 by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1); |
26 by (fast_tac (claset() addSIs [lepoll_1_is_sing]) 1); |
26 by (fast_tac (claset() addSIs [lepoll_1_is_sing]) 1); |
27 by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1); |
27 by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1); |
28 qed "eqpoll_1_iff_singleton"; |
28 qed "eqpoll_1_iff_singleton"; |
29 |
29 |
30 Goalw [succ_def] |
30 Goalw [succ_def] "[| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; |
31 "!!x. [| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; |
|
32 by (fast_tac (claset() addSEs [cons_eqpoll_cong, mem_irrefl]) 1); |
31 by (fast_tac (claset() addSEs [cons_eqpoll_cong, mem_irrefl]) 1); |
33 qed "cons_eqpoll_succ"; |
32 qed "cons_eqpoll_succ"; |
34 |
33 |
35 Goal "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}"; |
34 Goal "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}"; |
36 by (rtac equalityI 1); |
35 by (rtac equalityI 1); |