Proof of `Provable simplification of drops`
groundedproofs/Lax149335Proofs/Results/GeneralCompleteness.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 a syntactic analysis of drops: drops with co-product, product and list codomains are normalised, the normal forms of two drops are brought to a common shape by a common lift, and a drop of that shape into the lists over a finite alphabet is provably equivalent to a simple rational term.