Say that I want to relate “types” generated by Ott to Coq types:

```
Inductive typ : Set := typ_nat | typ_bool.
Definition type_of_typ (t : typ) : Type :=
match t with
| typ_nat => nat
| typ_bool => bool
end.
Goal forall (t : typ),
type_of_typ t = nat ->
t = typ_nat.
intros t H; destruct t; auto; simpl in H.
Fail discriminate H.
```

The command has indeed failed with message:

Error: Ltac call to “discriminate (destruction_arg)” failed.

Not a discriminable equality.

My questions are:

- Is this goal provable?
- What kinds of equalities are discriminable?