Hello!

I've been looking into the proof of `of_list_to_list_opp`

in the vector library trying to understand how it is proved without the axiom `eq_rect_eq`

and I see it uses `case0`

.

I was attempting to prove `case0`

on my own with tactics rather than by explicitly constructing a proof term as done in the standard library, but whenever I tried to destruct `v : VectorDef.t A 0`

I kept running into the error:

```
Error: Abstracting over the terms "n" and "v" leads to a term
λ (n0 : ℕ) (v0 : VectorDef.t A n0) ⇒ v0 = []
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"VectorDef.t A n0" : "Set"
"v0" : "VectorDef.t A n0"
"[]" : "VectorDef.t A 0"
The 3rd term has type "VectorDef.t A 0" which should be coercible to "VectorDef.t A n0".
```

Is there a way to destruct terms of dependent types without appealing to tactics that use axioms such as `dependent destruction`

?

Thanks!

Equations' tactics are much better at avoiding axiom K

(Equations = the Coq-Equations library/Coq plugin)

moreover, using `Vector`

without using Coq-Equations is typically discouraged.

in part because of errors like the one you see

Last updated: Feb 04 2023 at 22:29 UTC