Proof of `Lift-drop factorisation`
groundedproofs/Lax149335Proofs/Results/GeneralCompleteness.lean · lax-149335
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
By induction on the term. The atomic terms are factorised directly, the functoriality combinators preserve factorisations, and for a composition the inner drop-lift is turned into a lift-drop by the exchange lemma.