proposition: Lemma semBindSizeEnum A B (g : E A) (f : A -> E B) (s : nat) : semEnumSize (bindEnum g f) s <--> \bigcup_(a in semEnumSize g s) semEnumSize (f a) s.
proof: Proof. rewrite /semEnumSize /bindEnum /=. unfold bindLazyList. generalize (run g s). induction l. - simpl. split; intros; try contradiction. inv H. destruct H0. contradiction. - simpl in *. intros z; split; intros H1. + eapply lazy_in_app_or in H1. inv H1. * eexists. split. left. reflexivity. eassumption. * eapply H in H0. inv H0. destruct H2. eexists. split. right. eassumption. eassumption. + inv H1. destruct H0. inv H0. * eapply lazy_append_in_l. eassumption. * eapply lazy_append_in_r. eapply H. eexists. split; eauto. 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)