Commit 2024-01-19 22:02 a3794dc0
View on Github →feat(Data/Set/Finite): Induction principle for Set (#9123)
This PR adds another induction principle for Set where you prove that a property C holds of Set.univ by proving the inductive step C S → ∃ a ∉ S, C (insert a S) (the key being exists the use of exists rather than forall).