proposition: Lemma list_forall_impl : forall (A : Type) (f f' : A -> bool) (l : list A), (forall a, In a l -> f a = true -> f' a = true) -> (list_forall f l) = true -> (list_forall f' l) = true.
proof: Proof. intros A f f' l; induction l as [ | a l]; simpl; trivial. intros Hl; assert (Ha := Hl a (or_introl _ (eq_refl _))). destruct (f a); simpl. intro H; rewrite IHl; simpl; trivial. rewrite (Ha (eq_refl _)); trivial. intros; apply Hl; trivial; right; trivial. intro; absurd (false = true); trivial; discriminate. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)