# Error-uniform-shortcut-laws


fx.experimental.desc-interp.effects.error-uniform-shortcut-laws: kernel-checked H.refl lemmas certifying that each `uniformOf_*` on the canonical EffError raise reduces to the appropriate `mkResumeAt`/`mkAbortAt` UniRet form. All three `uniformOf_X` are defined as direct `EffError.elim 0`-dispatches; at the canonical `error E payload` op, ι on the elim fires (single constructor → onError branch) and β on the onError λs delivers the RHS in one normal-form step. So all three lemmas discharge by H.refl uniformly.

## `collectingUniformLemma`

_Proof of collecting-uniform lemma: single H.refl over `uniformOf_collecting`'s direct `EffError.elim 0` dispatch at the canonical `error` constructor. ι + two β. Kernel typing of mkResume's r-slot additionally requires `Resp_collecting E op ≡_ι Unit`, which the same ι firing delivers._

## `collectingUniformLemmaTy`

_Π-type of collecting-uniform lemma: `Π E A. Π payload:E. Π s:List E. uniformOf_collecting E A (error E payload) s ≡ mkResumeAt (List E) Ee Resp_collecting_E op A tt (cons E payload s) : UniRet (List E) Ee Resp_collecting_E op A`._

## `resultUniformLemma`

_Proof of result-uniform lemma: single H.refl over `uniformOf_result`'s direct `EffError.elim 0` dispatch at the canonical `error` constructor. ι + two β; the onError branch's body emits `mkAbort … (inl E A_inner payload) _s` directly._

## `resultUniformLemmaTy`

_Π-type of result-uniform lemma: `Π E State A_inner. Π payload:E. Π s:State. uniformOf_result E State A_inner (error E payload) s ≡ mkAbortAt State Ee Resp_result_E op (Sum E A_inner) (inl E A_inner payload) s : UniRet State Ee Resp_result_E op (Sum E A_inner)`._

## `strictUniformLemma`

_Proof of strict-uniform lemma: single H.refl over `uniformOf_strict`'s direct `EffError.elim 0` dispatch at the canonical `error` constructor. ι + two β._

## `strictUniformLemmaTy`

_Π-type of strict-uniform lemma: `Π E State. Π payload:E. Π s:State. uniformOf_strict E State (error E payload) s ≡ mkAbortAt State Ee Resp_strict_E op E payload s : UniRet State Ee Resp_strict_E op E`._