| changeset 76214 | 0c18df79b1c8 |
| parent 76213 | e44d86131648 |
| child 76215 | a642599ffdea |
--- a/src/ZF/ex/CoUnit.thy Tue Sep 27 16:51:35 2022 +0100 +++ b/src/ZF/ex/CoUnit.thy Tue Sep 27 17:03:23 2022 +0100 @@ -55,7 +55,7 @@ inductive_cases Con2E: "Con2(x, y) \<in> counit2" -lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'" +lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' \<and> y = y'" \<comment> \<open>Proving freeness results.\<close> by (fast elim!: counit2.free_elims)