proposition: Lemma segment_closed_suffix (A : UU0) (p : segment_closed.t A) s : ~~ p s -> forall t, ~~ p (s ++ t).
proof: Proof. move=> ps t; apply: contra ps; by case/segment_closed.H. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib