# 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`._