proposition: Lemma lazylist_backtrack_opt_true A (l: LazyList.LazyList (option A)) ch b : lazylist_backtrack_opt l ch b = Some true <-> exists x, LazyList.In_ll (Some x) l /\ ch x = Some true.
proof: Proof. revert b; induction l; intros b. - simpl. split; intros Hc; try congruence. destruct b; congruence. destruct Hc. inv H; exfalso; eauto. - split. + intros Hl. simpl in *. destruct a. destruct (ch a) eqn:Heq. * destruct b0. -- eexists. split; eauto. -- eapply H in Hl. destruct Hl. inv H0. eexists; split; eauto. * eapply H in Hl. destruct Hl. inv H0. eexists; split; eauto. * eapply H in Hl. destruct Hl. inv H0. eexists; split; eauto. + intros Hc; inv Hc. inv H0. simpl in *. destruct a. * inv H1. inv H3. rewrite H2. reflexivity. destruct (ch a) eqn:Heq. destruct b0. reflexivity. eapply H. eexists. now split; eauto. eapply H. eexists. now split; eauto. * inv H1. congruence. eapply H. eexists. now split; eauto. Qed.
imports: Coq.Classes.Morphisms mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat) Sets Tactics Recdef List ZArith ZArith.Znat Arith Producer Generators Enumerators