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