Proof of `Injective string representations`
groundedproofs/Lax149335Proofs/Results/Preliminaries.lean · lax-149335
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
A type is first encoded injectively into strings over a finite alphabet, by induction on the type, and the finite alphabet is then encoded into binary strings by blocks of a fixed length that is a power of two, using the injectivity half of the bundle lemma.