The internal development proves the statement for classes indexed by arbitrary finite vertex types. The submitted class $C$ is therefore closed under subgraph copies — the closure is nowhere dense in the internal sense as soon as $C$ is nowhere dense in the submitted sense, since a internal minor model of a clique in a copy pushes forward to a submitted minor model in the host — the internal theorem is applied to the closure, and the conclusion is specialized back to the members of $C$ themselves. What remains is packaging: the internal statement is phrased with $Finset$ and $card$, the submitted one with $Set$ and $Set.ncard$, and the two are matched by $Set.toFinset$ and $Set.ncard_coe_finset$. Distance independence and vertex deletion need no translation at all: the internal step-reduction modules are stated over the definitions of the submitted concept.

The internal induction alternates an odd and an even distance-reduction step and consumes Ramsey's theorem twice — directly, to extract a homogeneous set, and through the bipartite Ramsey lemma (Lemma 3.9 of the notes) — so both Ramsey statements of the $finite-ramsey$ submission are assumed rather than reproved here.

The statement is Lemma 3.4 of Chapter 4 of the sparsity lecture notes of Pilipczuk and Siebertz (numbering of the 2019/20 edition), the hard direction of their Theorem 3.2. The internal type-polymorphic version is $Lax12Proofs.QuasiWidenessInduction.nd_implies_uqw$.