theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
intros 2; cases H; clear H;
cut (a ◃ S' a);
- [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]]
+ [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); apply iter; autobatch]]
cut (a ◃ emptyset);
[2: apply transitivity; [apply (S' a)]
[ assumption