proposition: Lemma list_exists_app : forall (A : Type) (f : A -> bool) (l1 l2 : list A), list_exists f (l1 ++ l2) = orb (list_exists f l1) (list_exists f l2).
proof: Proof. intros A f l1; induction l1 as [ | a1 l1]; simpl; trivial. intro l2; rewrite (IHl1 l2); destruct (f a1); simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)