proposition: Lemma fold_left_and_false: forall (A: Type) ls (f: A -> bool), fold_left (fun b l => b && f l) ls false = false.
proof: Proof. intros. induction ls. simpl. reflexivity. simpl. assumption. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)