diff --git a/tests/gmap.v b/tests/gmap.v index 3eb98b0619ee09a6c29f59acc8ce10f4e8afb1b2..fff2df33a33d84a01b1ac8737b2974b467a1365d 100644 --- a/tests/gmap.v +++ b/tests/gmap.v @@ -82,3 +82,10 @@ Proof. Fail progress simplify_eq. done. Qed. + +(** Test case for issue #139 *) + +Lemma test_issue_139 (m : gmap nat nat) : ∃ x, x ∉ dom m. +Proof. + destruct (exist_fresh (dom m)); eauto. +Qed.