manage option "proofs" within theory context -- with minor overhead for primitive inferences;