proposition: Lemma promotable_enum : promotable is_iota are_adjacent.
proof: Proof. move=> s t Hs Ht. rewrite /is_iota /= size_cat iotaD. case/boolP : (nilp s) => [/nilP ->{Hs s} /=|s0]; first by rewrite addn0 /are_adjacent. rewrite /nilp -lt0n in s0. have -> : head 0 (s ++ t) = head 0 s by rewrite -nth0 nth_cat sub0n s0. rewrite -(eqP Hs) /are_adjacent /= -size_eq0 -(negbK (size s == _)) -lt0n s0 /=. rewrite eqseq_cat // eqxx /=. case/boolP : (nilp t) => [/nilP {Ht} ->{t} //|t0]. rewrite /nilp -lt0n in t0. rewrite -(size_eq0 t) -(negbK (size t == _)) -lt0n t0 /=. case: t Ht t0 => // a b Hab _. rewrite [head _ (_ :: _)]/=. rewrite is_iota_head_last //= eqseq_cons eq_sym andb_idr // => /eqP Ha. move: Hab. by rewrite /is_iota /= => /eqP[] {1}->; rewrite -Ha. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib