proposition: Lemma guardPn (b : bool) : if_spec b skip fail (~~ b) b (guard b).
proof: Proof. by rewrite /guard; unlock; case: ifPn => ?; constructor. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)