Proof of `Synchronised output lengths`
groundedproofs/Lax149335Proofs/Results/RationalFunctions.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
Compare the outputs on inputs that differ by one element in a single list component.