Decoder round trips and exact rejection

The position lemmas recover relation tables and the unique value of each constant. Re-encoding validation gives soundness for every input string.

theorem Complexity.DescriptiveComplexity.readStructCandidate_encodeStruct_internal {V : Vocabulary} (A : DecFinStruct V) : readStructCandidate V A.card ⋯ (encodeStruct A) = A

theorem Complexity.DescriptiveComplexity.decodeStruct_encodeStruct_internal {V : Vocabulary} (A : DecFinStruct V) : decodeStruct V (encodeStruct A) = some A

theorem Complexity.DescriptiveComplexity.decodeStruct_sound_internal {V : Vocabulary} (bits : List Bool) (A : DecFinStruct V) (h : decodeStruct V bits = some A) : encodeStruct A = bits