proposition: Lemma enumerate_SizeMonotonic (A : Type) (l : list (E (option A))) : l \subset SizeMonotonic -> SizeMonotonic (enumerate l).
proof: Proof. intros Hin. intros s1 s2 Hleq. rewrite !enumerate_correct_size'. intros x Hin'. destruct Hin' as [e [Hl Hs]]. eexists. split; eauto. eapply Hin; eauto. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)