proposition: Lemma list_forall_is_sound : forall (A : Type) P_bool (l : list A), list_forall P_bool l = true <-> (forall a, In a l -> P_bool a = true).
proof: Proof. fix list_forall_is_sound 3. intros A P_bool l; case l; clear l; simpl. split. intros _ a Abs; contradiction. intros _; reflexivity. intros a l; split. case_eq (P_bool a); intro Pa; simpl. intros Pl b b_in_al; case b_in_al; clear b_in_al. intro a_eq_b; subst b; exact Pa. revert b; rewrite <- (list_forall_is_sound A P_bool l); exact Pl. intro Abs; discriminate. intros Pal; rewrite (Pal a (or_introl _ (eq_refl _))); simpl. rewrite (list_forall_is_sound A P_bool l). intros b b_in_l; apply Pal; right; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)