mathlib3

feat(data/W): show finitely branching W types are encodable

#1817

Merged