proposition: Lemma subs_cat (xs ys : seq A) : (subs (xs ++ ys) = do us <- subs xs; do vs <- subs ys; Ret (us ++ vs))%Do.
proof: Proof. elim: xs ys => [ys |x xs ih ys]. by rewrite cat0s /= bindretf bindmret. rewrite {1}[in RHS]/subs fmapE -/(subs _) alt_bindDl bindA. Open (X in subs xs >>= X). rewrite bindretf. under eq_bind do rewrite cat_cons. over. rewrite [X in _ = X [~] _](_ : _ = fmap (cons x) (do x0 <- subs xs; do x1 <- subs ys; Ret (x0 ++ x1)))%Do; last first. rewrite fmapE bindA. bind_ext => x0. rewrite bindA. by under [in RHS]eq_bind do rewrite bindretf. by rewrite -ih cat_cons subs_cons. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)