Error-shortcut-laws

fx.experimental.desc-interp.effects.error-shortcut-laws: kernel-checked one-shot lemmas for each handle_* on the canonical EffError raise. Each lemma discharges by H.refl — ι on EffError.elim fires at the single error constructor, then β reduces the onError branch to a bare H.pair _ _. RHSes match extract.PairRaw emitter output, anchoring per-strategy shortcut soundness at the kernel layer.

collectingRaiseLemma

Proof of collecting-raise lemma: 3 lams + H.refl. State specialised to List E; onError cons-es payload onto the prior list and signals resume via tt.

collectingRaiseLemmaTy

Π-type of collecting-raise lemma: Π E. Π payload:E. Π s:List E. handle_collecting E (error E payload) s ≡ H.pair (H.cons E payload s) H.tt : Σ (List E) Unit.

resultRaiseLemma

Proof of result-raise lemma: 5 lams + H.refl. Always aborts; the Sum E A_inner result channel always carries the inl-injected payload (handler never produces inr).

resultRaiseLemmaTy

Π-type of result-raise lemma: Π E State A_inner. Π payload:E. Π s:State. handle_result E State A_inner (error E payload) s ≡ H.pair s (H.inl E A_inner payload) : Σ State (Sum E A_inner).

strictRaiseLemma

Proof of strict-raise lemma: 4 lams + H.refl. EffError has one constructor, so ι on EffError.elim 0 fires immediately at error; β on the onError λs (H.lam payload. H.lam _s. H.pair _s payload) yields H.pair s payload.

strictRaiseLemmaTy

Π-type of strict-raise lemma: Π E State. Π payload:E. Π s:State. handle_strict E State (error E payload) s ≡ H.pair s payload : Σ State E.