proposition: Theorem fold_left_orb_true_init : forall (A : Type)(f : A -> bool)(ls : list A), fold_left (fun b x => orb b (f x)) ls true = true.
proof: Proof. induction ls; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation