proposition: Lemma refin_if_guard (M : plusMonad) A (p : bool) (m1 m2 : M A) : (if p then m1 else m2) `<=` (guard p >> m1) [~] (guard (~~ p) >> m2).
proof: Proof. rewrite /refin; case: ifPn => /= [pT|pF]; rewrite !(guardT,guardF). by rewrite bindskipf bindfailf altA altmm. by rewrite bindfailf bindskipf altCA altmm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)