Two semantics in the repository define execution as a pair of mutually inductive relations: LeanExe.Wasi.Exec and LoopExec for WASI actions, and the Clight copy's exec_stmt and eval_funcall for the native path. A lemma about every execution needs induction over both relations at once. Lean rejects the ordinary routes, and the WASI and bare-metal work found the forms below independently.
For Exec and LoopExec, Lean rejected a recursive proof over the two relations, and the induction tactic does not apply to them. Apply the shared recursor with explicit motives, refine Exec.rec (motive_1 := fun {α} action world trace outcome final _ => …) (motive_2 := fun {α σ} remaining index state test step next world trace outcome final _ => …) ?_ … execution, with one goal for each constructor of both relations, as LeanExe.Wasi.Exec.not_trapped and Exec.bind do. Each motive binds every index of its relation, the implicit types included, and the second motive needs its own type variable σ because a loop's state type differs from the action's result. Later proofs over the resource semantics failed on motives left unopened in a case, on witness names reused across cases, and on existential predicates left uninstantiated, so each case must open its motive and name its variables afresh. The resource semantics has three relations and follows the same form with motive_3, as Verified.Wasi.Resource.ResourceExec.erase shows. A lemma about one loop can instead induct on the loop's remaining count and invert the derivation at each count, as LeanExe.Wasi.LoopExec.resume does.
The Clight copy lies in LeanExe/Native/Proof/, outside the libraries that the VKB check imports, so its lemmas are named here only. Lean's structural recursion over LClight.exec_stmt and eval_funcall needs every index of the recursive argument to be a variable. Write the two theorems in a mutual block that matches on the derivation and recurses on its sub-derivations, and replace a literal index by a variable with an equation: LClight.exec_stmt_ren in Rename.lean takes {e : env} (he : e = empty_env) where its statement would otherwise say empty_env. Put a second relation between the derivation's statement and another one after the derivation as its own hypothesis and split it with match, as LClight.exec_export_core in Export.lean takes CoreRel s' c. Running cases on the derivation's indices first rewrites the derivation's type, and Lean then rejects the recursive calls on it, so keep each derivation as it is and state the equations that cases would substitute as separate facts. LeanExe.Native.exec_quiet and funcall_quiet in Quiet.lean follow the same form, and the renaming and export proofs each met these limits.
The determinism proofs in LeanExe.Native.Clight.Determinism show the form inside the libraries that the check imports. LClight.exec_stmt_determ_prefix and LClight.eval_funcall_determ_prefix form a mutual block, each ending with termination_by structural h₁, with the second derivation and the other hypotheses after the colon. Each proof starts with match h₁ with, introduces the rest in each arm, and runs cases on the second derivation. cases h₁ in place of the match fails with "failed to infer structural recursion", because it rewrites the derivation that the recursion needs. Lean also promotes the uniform leading indices of a non-recursive inductive to parameters, such as chunk m b ofs of volatile_load, so cases … with | ctor names takes fewer names than the constructor's binders show and extra names fail with "Too many variable names provided". LClight.volatile_load_determ shows the right counts.