proposition: Lemma bind_ext_dassert (p : pred A) a (B : UU0) (m1 m2 : {x : A | p x} -> M B) : (forall x h, p x -> m1 (exist _ x h) = m2 (exist _ x h)) -> dassert p a >>= m1 = dassert p a >>= m2.
proof: Proof. move=> m1m2; have [pa|pa] := boolP (p a). by bind_ext => -[x px]; exact: m1m2. rewrite /dassert; case: Bool.bool_dec => [px|px]; first by rewrite px in pa. by rewrite !bindfailf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)