proposition: Lemma joinA_head a (c : C) (f : {hom c, M (M (M a))}) : [\o join _, M # join _, f] = [\o join _, join _, f].
proof: Proof. by rewrite compA joinA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)