haschu/nominal-lean.git/Nominal/Helpers/Finset.lean, branch main Formalization of nominal sets in Lean 4. https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Helpers/Finset.lean?h=main 2025-10-24T16:20:43Z use simp only everywhere except for last goal 2025-10-24T16:20:43Z Hannes Schulze haschu0103@outlook.de 2025-10-24T16:20:43Z urn:sha1:6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 Prove nonempty induction on finsets 2025-10-20T17:41:14Z Hannes Schulze haschu0103@outlook.de 2025-10-20T17:41:14Z urn:sha1:6dc12564566a00f24c1e03f83aa80b897ca71f56