Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `The conjugacy rule for syntactic conjugates`

groundedproofs/Lax149335Proofs/Results/SimpleCompleteness.lean · lax-149335

What this proof establishes

no assumptions

lem✓Lax149335.ConjugacyRule

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Both sides factor through the list of pairs (h(a),w)(h(a), w); the two factorisations are related by shifting the brackets of a list of pairs whose first components are values (the shift ones lemma) and naturality of shiftLshiftL.