proposition: Lemma algebraic_psi' (n : E ~> M) : algebraicity (psi' n).
proof: Proof. move=> A B g t. rewrite bindE. rewrite -(compE (M # g)). rewrite {1}/psi'. rewrite [in LHS](compA (M # g) Join). rewrite /=. rewrite -[in X in _ = Join X]compE. rewrite -[in RHS](natural n). transitivity (Join ((M # (Join \o (M # g))) (n (M A) t))); last first. rewrite -(compE _ (n (M A)) t). congr (Join ((M # _ \o _ ) t)). apply: boolp.funext => ma. by rewrite bindE. rewrite -[in X in Join X = _]compE. rewrite (natural join). rewrite functor_o. rewrite -[in RHS]FCompE. rewrite -[RHS]compE. rewrite [in RHS]compA. by rewrite joinA. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib