Proof of `Equivalence of simple rational terms is decidable`
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
By induction on the input type: over a co-product the two summands are compared, over a product each component is compared with the other one fixed, and over a list type the empty list and the singleton lists are compared; the last two cases are applications of Levi's lemma.