Logical story for tshell-call.
We use the
BOZO this probably isn't sound. Don't we get the equality axioms for tshell-call-fn1? But those aren't necessarily satisfied by command-line programs. We should probably be using oracle reads instead, but then we'll need to involve state.
Theorem:
(defthm return-type-of-tshell-call-fn1 (b* (((mv status lines) (tshell-call-fn1 cmd print save))) (and (natp status) (string-listp lines))))