proposition: Lemma aoperation_ext (f g : E.-aoperation M) : f = g <-> forall a, (f a = g a :> (_ -> _)).
proof: Proof. split => [ -> // |]; move: f g => [f Hf] [g Hg] /= fg. have ? : f = g by exact: funext_dep. subst g; congr (AOperation.Pack _). case: Hf => -[Hf1] [Hf2]. case: Hg => -[Hg1] [Hg2]. by f_equal; f_equal; exact/proof_irr. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy