equal
deleted
inserted
replaced
867 lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)" |
867 lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)" |
868 apply (induct_tac n) |
868 apply (induct_tac n) |
869 apply (simp add: eqpoll_0_iff, clarify) |
869 apply (simp add: eqpoll_0_iff, clarify) |
870 apply (subgoal_tac "EX u. u:A") |
870 apply (subgoal_tac "EX u. u:A") |
871 apply (erule exE) |
871 apply (erule exE) |
872 apply (rule Diff_sing_eqpoll [THEN revcut_rl]) |
872 apply (rule Diff_sing_eqpoll [elim_format]) |
873 prefer 2 apply assumption |
873 prefer 2 apply assumption |
874 apply assumption |
874 apply assumption |
875 apply (rule_tac b = A in cons_Diff [THEN subst], assumption) |
875 apply (rule_tac b = A in cons_Diff [THEN subst], assumption) |
876 apply (rule Fin.consI, blast) |
876 apply (rule Fin.consI, blast) |
877 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) |
877 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) |