proposition: Lemma lazylist_backtrack_opt_is_false A (l: LazyList.LazyList (option A)) ch b : lazylist_backtrack_opt l ch b = Some false -> b = false.
proof: Proof. revert b; induction l; intros b. - simpl. destruct b; try congruence. - simpl in *. destruct a. + destruct (ch a) eqn:Heq. destruct b0. congruence. now eauto. intros Hin. eapply H in Hin. congruence. + intros Hn. eapply lazylist_backtrack_opt_is_true in Hn. congruence. Qed.
imports: Coq.Classes.Morphisms mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat) Sets Tactics Recdef List ZArith ZArith.Znat Arith Producer Generators Enumerators