Factor the TypeOK inductive step out as LEMMA TypeOKStep - #217

Open

lemmy wants to merge 1 commit into

Commits on Jul 30, 2026

Prove Safety relative to TypeOK instead of via a combined invariant

lemmy
and
claude
committed