proposition: Lemma commutativity_of_assertions A q : Join \o (M # (bassert q)) = bassert q \o Join :> (_ -> M A).
proof: Proof. by apply funext => x; rewrite !compE join_fmap /bassert joinE bindA. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)