proposition: Lemma dlabels_relabel_is_fold : relabel >=> dlabels = foldt drTip drBin.
proof: Proof. apply foldt_universal. rewrite kleisli_def -3!compA. rewrite (_ : relabel \o Tip = (M # Tip) \o const fresh) //. rewrite (compA (fmap dlabels)) -functor_o. rewrite (_ : dlabels \o Tip = ret _ \o wrap) //. rewrite functor_o. by rewrite compA (compA Join) joinMret compidf. rewrite [in LHS]kleisli_def -(compA _ relabel). rewrite (_ : _ \o _ Bin = (fmap (uncurry Bin)) \o mpair \o relabel^`2); last first. by rewrite boolp.funeqE; case. rewrite -(compA (fmap (uncurry Bin))) -compA (compA (fmap dlabels)) -functor_o. rewrite (_ : _ \o _ Bin = (fmap ucat) \o bassert q \o mpair \o dlabels^`2); last first. by rewrite boolp.funeqE; case. transitivity ((fmap ucat) \o Join \o (fmap (bassert q \o mpair)) \o mpair \o (fmap dlabels \o relabel)^`2). rewrite [in RHS]natural -3![in RHS]compA; congr (_ \o _). rewrite -[in RHS]naturality_mpair 2![RHS]compA; congr (_ \o _). by rewrite -[X in _ = X \o _]functor_o -[RHS]functor_o -compA. rewrite -(compA (fmap ucat)) [X in Join \o X]functor_o (compA Join). rewrite commutativity_of_assertions. rewrite -(compA _ Join) (compA _ (bassert q)). rewrite -(compA _ _ mpair) -(compA _ (_ \o mpair)). by rewrite join_and_pairs. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib