proposition: Lemma enumerate_SizeFP (A : Type) (l : list (E (option A))) : l \subset SizeFP -> l \subset SizeMonotonicOpt -> SizeFP (enumerate l).
proof: Proof. intros Hin Hmon. intros s1 s2 Hleq Hnin. rewrite !enumerate_correct_size'. intros x; split. - intros [e [Hl Hs]]. eexists. split. eassumption. destruct x. + eapply Hmon; eauto. + exfalso. eapply Hnin. eapply enumerate_correct_size'. eexists. split; eassumption. - intros [e [Hl Hs]]. destruct x. 2:{ exfalso. eapply Hnin. eapply enumerate_correct_size'. eexists. split. eassumption. eapply Hin; try eassumption. intros Hc. eapply Hnin. eapply enumerate_correct_size'. eexists. split; eassumption. } eexists. split. eassumption. eapply Hin; try eassumption. intros Hc. eapply Hnin. eapply enumerate_correct_size'. eexists. split; 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)