proposition: Lemma semBindOptSize_subset_compat_eq (A B : Type) (g g' : E (option A)) (f f' : A -> E (option B)) s : semProdSize g s <--> semProdSize g' s -> (forall (x : A), semProdSize g s (Some x) -> semProdSize (f x) s <--> semProdSize (f' x) s) -> semProdSize (bindOpt g f) s <--> semProdSize (bindOpt g' f') s.
proof: Proof. intros H1 H2 a. split. eapply semBindOptSize_subset_compat. rewrite H1. now eapply subset_refl. intros x Hin. rewrite H2; eauto. now eapply subset_refl. eapply semBindOptSize_subset_compat. rewrite H1. now eapply subset_refl. intros x Hin. rewrite H2; eauto. now eapply subset_refl. eapply H1; 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)