Proof of `Reduction to co-pairings of guarded terms`
groundedproofs/Lax149335Proofs/Results/SimpleCompleteness.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 value extraction, there is an isomorphism after which both terms are co-pairings of -guarded terms; the conclusion is transported back along this isomorphism.