proposition: Lemma sequence_cons (M : monad) A h (t : seq (M A)) : (sequence (h :: t) = do x <- h ; do vs <- sequence t ; Ret (x :: vs))%Do.
proof: Proof. by []. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)