Proof of `The FAF verifier as a finite local-test system` (6th statement)
groundedproofs/Lax323828Proofs/FAFLocalTests.lean · lax-323828
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
Multiply the independent choices of the reference question, extensions, reference functions, and CNA functions.