[Merged by Bors] - feat(Order/WellQuasiOrder): WellQuasiOrdered if onto homomorphous from a WellQuasiOrdered relation#39787

Hagb wants to merge 6 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

WuProver:WellQuasiOrder-ontoWuProver/mathlib4:WellQuasiOrder-ontoCopy head branch name to clipboard