Function prove_certify_check 

pub fn prove_certify_check(
    premises: &[ProofExpr],
    goal: &ProofExpr,
) -> VerifiedProof

Prove goal from premises, certify the derivation, and kernel-check it.

This is the canonical pipeline. Symbols are extracted from the premises and goal and registered in a fresh kernel context (predicates as Entity → Prop, constants as Entity); each premise is registered as a hypothesis using the same conversion the certifier uses for hypothesis lookup, so a registered premise is guaranteed to match.