https://github.com/nahcnuj/tibi/blob/58ea6126316a4ed4cf29c7b2aa7a9aa77bee90a3/Tibi/Props/Compiler.lean#L7 ```text namespace Tibi -- TODO prove Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok /- type mismatch Wasm.Reduction.local__get ↑x.idx ```