fact: Fixpoint sequence (M : monad) A (s : seq (M A)) : M (seq A) := (if s isn't h :: t then Ret [::] else do v <- h; do vs <- sequence t; Ret (v :: vs))%Do.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)