proposition: Lemma enumeratingOpt_monotonic A (e : E (option A)) {Hc : SizeMonotonicOpt e} {Hfp : SizeFP e} ch1 ch2 s1 s2 b : (s1 <= s2)%coq_nat -> (forall x, ch1 x = Some b -> ch2 x = Some b) -> enumeratingOpt e ch1 s1 = Some b -> enumeratingOpt e ch2 s2 = Some b.
proof: Proof. intros Hleq Hall Hen. specialize (Hc _ _ Hleq). specialize (Hfp _ _ Hleq). unfold enumeratingOpt in *. unfold semProdSizeOpt in *. simpl in *. unfold semEnumSize in *. revert Hc Hfp Hen. generalize (run e s1), (run e s2). intros l1 l2 Hs1 Hs2 Hl. destruct b. - eapply lazylist_backtrack_opt_true in Hl. destruct Hl. destruct H. eapply lazylist_backtrack_opt_true. eexists. split. eapply Hs1. eassumption. eapply Hall. eassumption. - eapply lazylist_backtrack_opt_false in Hl. destruct Hl. eapply lazylist_backtrack_opt_false. split. intros x Hin. eapply Hall. eapply H. eapply Hs2. eassumption. eassumption. intros Hc. eapply H0. eapply Hs2. eassumption. eassumption. Qed.
imports: Coq.Classes.Morphisms mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat) Sets Tactics Recdef List ZArith ZArith.Znat Arith Producer Generators Enumerators