pub fn recheck(cert: &Certificate) -> Result<(), KernelError>Expand description
Independently re-validate a certificate.
Builds a fresh trusted context from the standard library, infers the type
of the certificate’s proof term, and requires it to match the claimed type
(up to definitional equality). Returns Ok(()) only if the proof genuinely
establishes the claimed proposition.
This function is the whole trusted core of an independent check. It does not look at where the certificate came from.