proposition: Lemma local_envTE (X : UU0) : (slifting local [the fmt of envT Z] naturality_MK) X = @local_envT' X.
proof: Proof. rewrite slifting_envT. by apply funext => -[]. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model