proposition: Lemma refin_alt A (m1 m1' m2 m2' : M A) : m1 `<=` m1' -> m2 `<=` m2' -> m1 [~] m2 `<=` m1' [~] m2'.
proof: Proof. by move=> h1 h2; rewrite /refin altACA h1 h2. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)