mathlib3

868333b9 - feat(data/W): show finitely branching W types are encodable (#1817)

feat(data/W): show finitely branching W types are encodable (#1817) * feat(data/equiv,data/fintype): an encodable fintype is equiv to a fin * feat(data/W): finitely branching W types are encodable * feat(archive/examples/prop_encodable): show a type of propositional formulas is encodable * fix(data/W): remove unused type class argument * fix(data/equiv): add two docstrings * fix(*): multiple fixes from code review Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>