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