Function emit_context 

pub fn emit_context(
    ctx: &Context,
    proofs: &(dyn Fn(&str) -> Option<Term> + Sync),
    target: &str,
) -> Result<EmittedDocument, Verdict>

emit_document over any checked context whose constants carry the importer’s key scheme. proofs hands back the checked proof of an opaque theorem, which a context does not keep.