proposition: Lemma enumerate_correct_opt {A} (lst : list (E (option A))) : semProdOpt (enumerate lst) <--> \bigcup_(x in lst) (semProdOpt x).
proof: Proof. unfold enumerate. induction lst. - rewrite bigcup_nil_set0. simpl. intros x; split; intros H; inv H; inv H0; inv H2. - simpl in *. split. + intros H1. unfold semEnumSize in *. inv H1. inv H. simpl in *. eapply lazy_in_app_or in H2. inv H2. * eexists. split. now left. eexists. split; eassumption. * assert (Hin : a0 \in \bigcup_(x in lst) (semProdOpt x)). { eapply IHlst. eexists. split; eassumption. } inv Hin. inv H4. eexists. split. right. eassumption. eassumption. + intros [b [H1 H2]]. inv H1. * unfold semEnumSize in *. simpl in *. inv H2. inv H. eexists. split. reflexivity. simpl. eapply lazy_append_in_l. simpl in *. eassumption. * assert (Hin : semProdOpt (MkEnum (fun s : nat => join_list_lazy_list (map (run^~ s) lst))) a0). { eapply IHlst. inv H2. inv H0. simpl. eexists. split; eauto. } inv Hin. inv H0. simpl. eexists. split. reflexivity. simpl in *. eapply lazy_append_in_r. simpl in *. 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)