proposition: Lemma lazylist_backtrack_opt_false A (l: LazyList.LazyList (option A)) ch : lazylist_backtrack_opt l ch false = Some false <-> (forall x, LazyList.In_ll (Some x) l -> ch x = Some false) /\ ~ LazyList.In_ll None l.
proof: Proof. induction l. - simpl. split; intros Hc. split; eauto. intros. now inv H. reflexivity. - split. + intros Hl. simpl in *. destruct a. * destruct (ch a) eqn:Heq. destruct b. congruence. -- eapply H in Hl. inv Hl. split. intros. inv H2; eauto. inv H3. eassumption. intros Hc; inv Hc. congruence. eauto. -- eapply lazylist_backtrack_opt_is_false in Hl. congruence. * eapply lazylist_backtrack_opt_is_false in Hl. congruence. + intros [H1 H2]. simpl. destruct a. * destruct (ch a) eqn:Heq. destruct b. rewrite H1 in Heq. congruence. now left. eapply H. split. intros. eapply H1. right. eassumption. intros Hc. eapply H2. right. eassumption. rewrite H1 in Heq. congruence. now left. * exfalso. eapply H2. now left. Qed.
imports: Coq.Classes.Morphisms mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat) Sets Tactics Recdef List ZArith ZArith.Znat Arith Producer Generators Enumerators