proposition: Lemma slifting_envT (X : UU0) : (slifting op [the fmt of envT Env] naturality_MK) X = @op' _.
proof: Proof. apply funext => emx. rewrite /op'. apply funext => s. rewrite /slifting. rewrite 2!vcompE. set h := hmap _. rewrite (psikE op). rewrite 2!functor_app_naturalE. rewrite /=. congr (from_component _). apply funext_dep => A; apply funext => f. rewrite {1}/psi' /=. rewrite /bindEnv /=. rewrite vcompE/=. rewrite bindE /= /bindK. rewrite fmapE /bindK. rewrite /liftEnv /=. rewrite -(compE _ _ emx) -functor_o. rewrite -[in RHS](compE _ _ emx) -functor_o. rewrite /psi' /= /bindK /= /kappa' /=. congr (op A). rewrite -(compE _ _ emx) -[in RHS](compE _ _ emx). by rewrite -2!functor_o. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer