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.