proposition: Lemma enumerate_SizeMonFP (A : Type) (l : list (E (option A))) : l \subset SizeFP -> l \subset SizeMonotonicOpt -> SizeMonotonicOptFP (enumerate l).
proof: Proof. intros H1 H2. constructor. eapply enumerate_SizeMonotonicOpt. eassumption. eapply enumerate_SizeFP; eassumption. 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)