recursor for FinEnum producing data

Stream: mathlib4

[Tom Kranz]

Would a recursor for FinEnum types, in the fashion of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Option.html#Fintype.truncRecEmptyOption (but producing non-truncated data), warrant inclusion in mathlib? I came across this whilst porting code that used the truncated version and wanted to make it produce data. I have a draft in that porting effort's branch over here: https://github.com/TpmKranz/mathlib4/blob/b53727b5dbb060d0d8c17987686c74ac5a15984e/Mathlib/Data/FinEnum/Option.lean