return to top
source
If e is an application of the form f a where f is an injective function in (← get).inj.fns, asserts f⁻¹ (f a) = a
e
f a
f
(← get).inj.fns
f⁻¹ (f a) = a