proposition: Lemma enumerate_correct_size' {A} (lst : list (E (option A))) s : semProdSize (enumerate lst) s <--> \bigcup_(x in lst) (semProdSize x s).
proof: Proof. unfold enumerate. induction lst. - rewrite bigcup_nil_set0. simpl. intros x; split; intros H; inv H. - simpl in *. split. + intros H1. unfold semEnumSize in *. simpl in *. eapply lazy_in_app_or in H1. inv H1. * eexists. split. now left. eassumption. * assert (Hin : a0 \in \bigcup_(x in lst) (semProdSize x s)). { eapply IHlst. eassumption. } inv Hin. inv H0. eexists. split. right. eassumption. eassumption. + intros [b [H1 H2]]. inv H1. * unfold semEnumSize in *. simpl in *. eapply lazy_append_in_l. eassumption. * simpl. eapply lazy_append_in_r. eapply IHlst. 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)