proposition: Lemma fold_left_and: forall (A: Type) ls (l: A) f, (fold_left (fun b l => b && f l) ls true = true /\ In l ls) -> f l = true.
proof: Proof. intros. destruct H. generalize dependent l. generalize dependent f. induction ls. intros. unfold In in H0. contradiction. intros. apply in_inv in H0. destruct H0. subst a. simpl in H. destruct (f l). reflexivity. simpl in H. rewrite fold_left_and_false in H. assumption. apply IHls. simpl in H. destruct (f a). assumption. rewrite fold_left_and_false in H. inversion H. assumption. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)