blob: d6720d99063241efbcbc77b9923c7aec1fff2eab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Inductive vector A : nat -> Type :=
|nil : vector A 0
|cons : forall (h:A) (n:nat), vector A n -> vector A (S n).
Global Set Mangle Names.
Lemma vlookup_middle {A n} (v : vector A n) : True.
Proof.
induction v as [|?? IHv].
all:exact I.
Qed.
|
