Function fol_to_model_checker_module 

pub fn fol_to_model_checker_module(
    premises: &[ProofExpr],
    goal: &ProofExpr,
    english: &str,
    fol: &str,
) -> String

Like fol_to_model_checker, but emits NO demo fn main — the form bundled into an imperative program’s mod proven (which has its own main). Produces only the World + holds (+ Monitor) library items.