proposition: Lemma refin_if (M : altMonad) A (m1 m2 m1' m2' : M A) (b : bool) : (b -> m1 `<=` m1') -> (~~ b -> m2 `<=` m2') -> (if b then m1 else m2) `<=` (if b then m1' else m2').
proof: Proof. by case: b => [+ _|_]; exact. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)