Proof of `Agreement among many decoded tables` (2nd statement)
groundedproofs/Lax253009Proofs/ManyTableConsistency.lean · lax-253009
What this proof establishes
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
Choose one representative table for each selected value. Conditional on these tables, all remaining independent tables must hit their union. Sum over the at most 2^n possible representative sets.