proposition: Lemma join_and_pairs : (Join \o (M # mpair) \o mpair) \o ((fmap dlabels) \o relabel)^`2 = (mpair \o Join^`2) \o ((fmap dlabels) \o relabel)^`2.
proof: Proof. rewrite boolp.funeqE => -[x1 x2]. rewrite 3!compE. rewrite joinE. rewrite fmapE. rewrite 2![in RHS]compE. rewrite [in RHS]/mpair. rewrite [in LHS]/mpair. move H : (fmap dlabels) => h. rewrite /=. rewrite 2![in RHS]joinE. rewrite 3!bindA. rewrite -H. rewrite !fmapE. rewrite 3!bindA. bind_ext => {}x1. rewrite 2!bindretf 2!bindA. under eq_bind do rewrite 3!bindretf. rewrite -dlabelsC. bind_ext => ?. rewrite /=. rewrite bindA. by under [in RHS]eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib