: forall (A : Type) (v : {H : nat & vector A H}),
(fun H : {H : nat & vector A H} => orn_list_vector A (orn_list_vector_inv A H) = H) v
We want, for example:
: forall (A : Type) (v : {H : nat & vector A H}),
orn_list_vector A (orn_list_vector_inv A v) = v
We can pass this type to Coq. While we're at it, we can generate the section type (which Coq figures out fine) and pass it to Coq too, just so that we have an extra validation step.
The automatically generated type is, for example:
We want, for example:
We can pass this type to Coq. While we're at it, we can generate the section type (which Coq figures out fine) and pass it to Coq too, just so that we have an extra validation step.