Lessness has marked this topic as resolved.
Turns out even the
in is not needed, so it comes out to the remarkably concise:
Inductive vector A: nat -> Type := | vnil: vector A 0 | vcons: forall (n: nat), A -> vector A n -> vector A (S n). Theorem test A (v: vector A 0): v = vnil A. Proof. exact (match v with vnil _ => eq_refl end). Qed.
(I'm just a beginner, so I'm still working on understanding why this works...)
Last updated: Feb 09 2023 at 00:03 UTC