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