proposition: Lemma checker_backtrack_spec l : checker_backtrack l = Some true <-> exists f, List.In f l /\ f tt = Some true.
proof: Proof. unfold checker_backtrack. generalize false at 2. induction l. - intros b. destruct b; split; try (intros; congruence). * intros H. inv H. inv H0. inv H. * intros H. inv H. inv H0. inv H. - intros b. split. + intros H. destruct (a tt) eqn:Hdec. * destruct b0. exists a. split; eauto. now left. eapply IHl in H. destruct H. inv H. eexists; split; eauto. now right. * eapply IHl in H. destruct H. inv H. eexists; split; eauto. now right. + intros H. inv H. inv H0. inv H. rewrite H1. reflexivity. destruct (a tt). destruct b0. reflexivity. * eapply IHl. eexists. split; eauto. * eapply IHl. eexists. split; eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)