相关疑难解决方法(0)

我有一个类型定义为

Inductive bits : nat -> Set :=
| bitsNil : bits 0
| bitsCons : forall {l}, bool -> bits l -> bits (S l).

我试图证明：

Lemma emptyIsAlwaysNil : forall {a: bits 0}, a = bitsNil.

之后intros，我已经试过constructor 1，case a，intuition，无济于事。case a似乎是最接近的，但它得到一个错误：

Abstracting over the terms "0" and "a" leads to a term
fun (n : nat) (a0 : bits n) => a0 = bitsNil
which is ill-typed.
Reason is: Illegal …