changeset 76216 | 9fc34f76b4e8 |
parent 76215 | a642599ffdea |
child 76217 | 8655344f1cf6 |
--- a/src/ZF/AC/AC7_AC9.thy Tue Sep 27 17:46:52 2022 +0100 +++ b/src/ZF/AC/AC7_AC9.thy Tue Sep 27 17:54:20 2022 +0100 @@ -22,7 +22,7 @@ "C \<in> A \<Longrightarrow> (\<lambda>g \<in> (nat->\<Union>(A))*C. (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) " -apply (unfold inj_def) + unfolding inj_def apply (rule CollectI) apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) apply (rule fun_extension, assumption+)