proposition: Lemma promote_assert_sufficient_condition (M : failMonad) (A : UU0) : BindLaws.right_zero (@bind M) (@fail _) -> forall (p : segment_closed.t A) q, promotable p q -> promote_assert M p q.
proof: Proof. move=> right_z p q promotable_pq. rewrite /promote_assert; apply: boolp.funext => -[x1 x2]. rewrite 3![in RHS]compE [in RHS]fmapE. rewrite 2![in LHS]compE {1}/bassert [in LHS]bind_fmap !bindA. bind_ext => s. rewrite bindA; under eq_bind do rewrite bindretf. case: assertPn => ps; last first. rewrite bindfailf. With (idtac) Open (X in _ >>= X). rewrite /assert; unlock => /=. rewrite (negbTE (segment_closed_suffix ps x)) guardF bindfailf. reflexivity. by rewrite right_z. rewrite bindretf bindA /=. under [RHS]eq_bind do rewrite bindretf. rewrite bindA. bind_ext => t. case: (assertPn _ _ t) => pt; last first. rewrite bindfailf assertE (negbTE (segment_closed_prefix pt s)) guardF. by rewrite bindfailf. by rewrite bindretf /= 2!assertE promotable_pq //= bindA bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib