Rules for exec-expr-call.
Theorem:
(defthm exec-expr-call-open (implies (and (not (zp limit)) (equal vals (exec-expr-pure-list args compst)) (value-listp vals)) (equal (exec-expr-call fun args compst fenv limit) (exec-fun fun vals compst fenv (1- limit)))))