proposition: Lemma refin_liftM2 (M : plusMonad) (A B C : UU0) {f : A -> B -> C} {m1 n1 : M A} {m2 n2 : M B} : m1 `<=` n1 -> m2 `<=` n2 -> liftM2 f m1 m2 `<=` liftM2 f n1 n2.
proof: Proof. move=> mn1 mn2; rewrite /liftM2. by apply: (refin_bind mn1 _) => a; exact: refin_bindr. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)