diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-02 15:48:06 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-02 15:48:06 +0100 |
| commit | 996f75a7526591f89160b2df1d52cd5075696618 (patch) | |
| tree | e9445a811275e88fe350d560b8a0bfab35cdc8d5 /src/common | |
| parent | 385ac7a100a202886784ceecc1fa6c4836958f0b (diff) | |
| download | vericert-996f75a7526591f89160b2df1d52cd5075696618.tar.gz vericert-996f75a7526591f89160b2df1d52cd5075696618.zip | |
Finished the propert version of from_predicated_sem_pred_expr2
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 2169306..24a29a3 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -326,3 +326,15 @@ Proof. - constructor. - clear H. inv H1; intuition (constructor; auto). Qed. + +Lemma In_map2 : + forall A B (f: A -> B) n (x: B), + In x (map f n) -> + exists y, In y n /\ x = f y. +Proof. + induction n; inversion 1; subst; cbn in *. + - inv H. exists a; split; auto. constructor. + - clear H. inv H1. + + exists a; split; auto; constructor; tauto. + + exploit IHn; eauto; simplify. exists x0; split; auto; constructor; tauto. +Qed. |