# What I'm doing wrong? Smth not computing

```Require Import List Arith Utf8.
Set Implicit Arguments.

Definition dec (P: Prop) := { P } + { ~ P }.
Definition eq_dec A := ∀ (x y: A), { x = y } + { x ≠ y }.
Definition fmap A B (Da: eq_dec A) (Db: eq_dec B) :=
{ L: list (A * B) | NoDup (map fst L) }.

Definition fmap_value A B Da Db (m: @fmap A B Da Db) (key: A): option B.
Proof.
destruct m. induction x.
+ simpl in *. exact None.
+ simpl in *. apply NoDup_cons_iff in n. destruct n.
destruct (IHx H0).
- exact (Some b).
- destruct a. destruct (Da a key).
* exact (Some b).
* exact None.
Defined.
Definition all_keys A B Da Db (m: @fmap A B Da Db) :=
map fst (proj1_sig m).

Definition test_fmap: fmap Nat.eq_dec Nat.eq_dec.
Proof.
exists ((1,2)::(2,3)::(3,5)::nil).
simpl. apply NoDup_cons.
+ intro. simpl in H. intuition; congruence.
+ apply NoDup_cons.
- intro. simpl in H. intuition; congruence.
- apply NoDup_cons.
* intro. simpl in H. auto.
* apply NoDup_nil.
Defined.
Eval compute in (fmap_value test_fmap 2).```

The “Eval compute” doesn’t return Some 3 somehow.

As you can see it blocks on NoDup_cons_iff which is opaque.
You can change your definition to avoid this:

``````-  + simpl in *. apply NoDup_cons_iff in n. destruct n.
-    destruct (IHx H0).
+  + simpl in *. destruct IHx.
+    - apply NoDup_cons_iff in n. destruct n as [_ H0];apply H0.
``````

The main point is that the `destruct n` where `n` comes from the opaque proof is moved from the “main stream” of the definition (where it blocks everything) to only a subproof (where it only blocks the proof part).

1 Like