Recursion principle for Finset

Stream: Is there code for X?

[Geoffrey Irving]

Is there a recursion principle for Finset, analogous to Finset.induction but able to construct (dependent) types? I assume you'd have to pass in the fact that inserting elements in any order gives the same result.

[Violeta Hernández]

#mwe?

[Aaron Liu]

Try docs#Multiset.rec

[Geoffrey Irving]

^ Thanks, that looks reasonable!