proposition: Lemma handle_exceptTE (X : UU0) : (slifting handle [the fmt of exceptT Z] naturality_MK) X = @handle_exceptT' X.
proof: Proof. by rewrite slifting_exceptT; exact: funext. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model