Proof of `Normalisation of values`
groundedproofs/Lax149335Proofs/Results/Preliminaries.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
Every term composed with the value representing an element of a type is provably equivalent to the value representing the image of that element; the lemma is the special case of a value applied to the unique element of .