losEval compute El comando no siempre se evalúa como una expresión simple. Considera el código:

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Qed.

Y, si ejecuto el siguiente comando:

Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2).

Coq me dice que el resultado es2. Sin embargo, cuando ejecuto la siguiente expresión:

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

Obtengo una expresión larga donde el predicado interno parece estar desplegado, pero no se da ningún resultado.

¿Qué tengo que cambiar para obtener la respuesta?1 en el últimoEval compute línea?