proposition: Lemma symbols_prop2 : symbols \o uaddn = (fmap ucat) \o mpair \o (symbols : _ -> M _)^`2.
proof: Proof. apply: boolp.funext => -[n1 n2]. elim: n1 => [|n1 IH]. rewrite [in LHS]compE uaddnE add0n. rewrite compE [in X in _ = _ X]/= squaringE symbols0. rewrite compE [in RHS]fmapE bindA bindretf. rewrite -fmapE fmap_bind. Open (X in _ >>= X). rewrite fcompE fmapE bindretf /=; reflexivity. by rewrite bindmret. rewrite compE uaddnE addSn symbolsS -uaddnE -(compE symbols) {}IH. rewrite [in RHS]compE [in X in _ = _ X]/= squaringE symbolsS. rewrite [in RHS]compE -/(fmap _ _) fmap_bind bindA; bind_ext => a. rewrite 2![in LHS]compE [in LHS]fmap_bind [in LHS]bindA [in RHS]bindA. bind_ext => s. rewrite [in RHS]bindretf [in RHS]fcompE [in RHS]fmap_bind. rewrite [in LHS]fcompE [in LHS]bind_fmap [in LHS]bindA. under eq_bind do rewrite bindretf. by under [RHS]eq_bind do rewrite fcompE fmapE bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib