Elaboration of serialized ZF expressions #
The implementation is imported at the meta phase so its expression decoders can execute inside term elaborators while their data definitions and correctness lemmas remain available.
The implementation is imported at the meta phase so its expression decoders can execute inside term elaborators while their data definitions and correctness lemmas remain available.