Rules for exec-initer.
Theorem:
(defthm exec-initer-when-single (implies (and (syntaxp (quotep initer)) (equal (initer-kind initer) :single) (not (zp limit)) (equal expr (initer-single->get initer)) (equal val+compst1 (exec-expr-call-or-pure expr compst fenv (1- limit))) (equal val (mv-nth 0 val+compst1)) (equal compst1 (mv-nth 1 val+compst1)) (valuep val)) (equal (exec-initer initer compst fenv limit) (mv (init-value-single val) compst1))))