proposition: Theorem fold_and_false_init : forall (A : Type)(ls : list A) P, fold_left (fun b z => b && negb (P z)) ls false = false.
proof: Proof. induction ls; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation