From fc4bc25ca5d986831a02cddd87264b7b51943fc4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 May 2023 14:42:03 +0100 Subject: Prove evaluable_pred_expr_exists_RBsetpred --- src/common/NonEmpty.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/common') diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 3aff11d..2c3ae94 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -292,3 +292,16 @@ Proof. inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H. cbn. f_equal. eauto. Qed. + +Lemma Forall_forall: + forall (A : Type) (P : A -> Prop) (l : non_empty A), Forall P l <-> (forall x : A, In x l -> P x). +Proof. + induction l. + - split; intros. + + inv H. inv H0. auto. + + constructor. specialize (H a). apply H. constructor. + - split; intros. + + inv H. inv H0. inv H1; eauto. eapply IHl in H4; eauto. + + constructor. eapply H. constructor; tauto. eapply IHl. + intros. eapply H. constructor; tauto. +Qed. -- cgit