proposition: Theorem uniform_algebraic_lifting : lifting op e alifting.
proof: Proof. move=> X. apply: boolp.funext => Y. rewrite /alifting. rewrite [in RHS]/=. rewrite psiE. rewrite vcompE. rewrite phiE. rewrite !compE. rewrite (_ : (E # Ret) ((E # e X) Y) = (E # (M # e X)) ((E # Ret) Y)); last first. rewrite -[in LHS]compE -functor_o. rewrite -[in RHS]compE -functor_o. by rewrite (natural ret) FIdE. set x := (Z in Join (e (N X) Z)). rewrite (_ : x = (M # e X) (op (M X) ((E # Ret) Y))); last first. rewrite -(compE (M # e X)). by rewrite (natural op). transitivity (e X (Join (op (M X) ((E # Ret) Y)))); last first. rewrite joinE. rewrite monadMbind. rewrite bindE -(compE _ (M # e X)). by rewrite -natural. by rewrite -[in LHS](phiK op). Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib