proposition: Theorem fold_left_orb_all_false : forall (A : Type)(ls : list A), fold_left (fun b _ => orb b false) ls false = false.
proof: Proof. induction ls; intuition idtac; simpl in *. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation