proposition: Lemma slifting_exceptT (X : UU0) : (slifting op [the fmt of exceptT Z] naturality_MK) X = @op' X.
proof: Proof. apply funext => emx. rewrite /op'. rewrite (psikE op (Z + X)%type). rewrite /slifting. rewrite 2!vcompE. set h := hmap _. rewrite /=. f_equal. rewrite /psi' /=. rewrite /bindX bindE /=. apply funext_dep => A; apply funext => k. rewrite vcompE/=. rewrite /liftX /=. rewrite bindE /= /bindK /=. rewrite /psi' /= /bindK /=. rewrite /kappa' /=. congr (op _ _). rewrite -(compE (E # _)). by rewrite -functor_o. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer