proposition: Lemma eq_idx_spec : forall i j, decide_spec (@eq _) i j (eq_idx_bool i j).
proof: Proof. induction i; destruct j; simpl; try (constructor; congruence). case (IHi j); constructor; congruence. case (IHi j); constructor; congruence. Qed.
imports: Coq(Arith NArith List RelationClasses)