proposition: Lemma refin_trans A (b a c : M A) : a `<=` b -> b `<=` c -> a `<=` c.
proof: Proof. by rewrite /refin => h1 <-; rewrite altA h1. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)