proposition: Lemma assertPn {A : UU0} (p : pred A) (a : A) : if_spec (p a) (Ret a) fail (~~ (p a)) (p a) (assert p a).
proof: Proof. rewrite assertE; case: guardPn => pa; by [rewrite bindskipf; constructor | rewrite bindfailf; constructor]. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)