Function fol_to_model_checker 

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

Emit a self-contained Rust rule module for premises ⊨ goal (empty premises = check the single formula goal). english/fol are echoed as doc comments.