Function prove_library_with_axioms 

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

Like prove_library but with a shared axioms base in scope for every theorem — a named theory (e.g. the Tarski geometry axioms) on which the whole dependency graph is discharged.