Function prove_scripted_library 

pub fn prove_scripted_library(
    axioms: &[ProofExpr],
    theorems: &[ScriptedTheorem],
) -> Vec<LibraryResult>

Discharge a library of scripted theorems in citation order, on a shared axioms base. Each theorem is proved by its ScriptedTheorem::script from its premises, the axioms, and the conclusions of the theorems it cites (already proved); a proved conclusion becomes a citable lemma for later theorems — the scraped-Euclid-graph discipline, now driven by tactic scripts. Results come back in INPUT order.