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?