Collect expressions used in right-hand side positions (and if-statement conditions.)
(vl-stmt-cblock-rvalexprs x) → exprs
Theorem:
(defthm return-type-of-vl-stmt-cblock-rvalexprs.exprs (implies (and (force (vl-stmt-p x)) (force (vl-stmt-cblock-p x))) (b* ((?exprs (vl-stmt-cblock-rvalexprs x))) (vl-exprlist-p exprs))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-stmtlist-cblock-rvalexprs.exprs (implies (and (force (vl-stmtlist-p x)) (force (vl-stmtlist-cblock-p x))) (b* ((?exprs (vl-stmtlist-cblock-rvalexprs x))) (vl-exprlist-p exprs))) :rule-classes :rewrite)