Function emit_property_check 

pub fn emit_property_check(
    ctx: &Context,
    name: &str,
    prop: &Term,
) -> Option<String>

Emit a runnable property check fn check_<name>(params) -> bool { … } from a theorem’s PROPOSITION (its kernel type), or None if the statement isn’t a finite, executable property over extractable functions. A proven theorem like ∀n. Eq Nat (add Zero n) n becomes fn check_…(n: Nat) -> bool { add(Nat::Zero, n) == n }.