proposition: Lemma promotable_uniq_seq_disjoint A : promotable (@uniq A) seq_disjoint.
proof: Proof. move=> s t ps pt. by rewrite cat_uniq ps pt /= andbT -nilp_intersect. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib