proposition: Lemma guard_and a b : guard (a && b) = guard a >> guard b.
proof: Proof. move: a b => -[|] b /=; by [rewrite guardT bindskipf | rewrite guardF bindfailf]. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)