diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
| commit | fc4bc25ca5d986831a02cddd87264b7b51943fc4 (patch) | |
| tree | 075f6cf97f3a35a0c6d34650806b295573288c5f /src/common | |
| parent | 28352e0b7c53f7b0d3e610bf8507ee4b0901171d (diff) | |
| download | vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.tar.gz vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.zip | |
Prove evaluable_pred_expr_exists_RBsetpred
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 13 |
1 files changed, 13 insertions, 0 deletions
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. |