Description: Type-safe pets scheme. On a membership block-carrier
A e. MembParts , the lifted span ( R |X. (`' _E |`A ) ) yields
a generalized partition of A iff its coset relation yields an
equivalence relation on the same carrier A . This is the type-safe
replacement for the earlier broad pets : it explicitly restricts to
carriers where A is already known to be a block-family (by
MembParts ). That removes the standard type-safety objection ("are
you equating a quotient-carrier of blocks with raw witnesses?") by
construction. It is the key bridge used to identify the partition-side
and equivalence-side pet classes ( petseq ), in complete parallel with
the membership bridge mpets . This theorem is intentionally not the
definition of PetParts ; it is the bridge used by petseq after
typedness is enforced by the "Pet*" definitions. (Contributed by Peter
Mazsa, 19-Feb-2026)