A bit of a mechanical question regarding Coq Vectors. In my proof I have
input: Vector.t nat 1
==================================
compliacted_fixpoint_for input = true
I am looking for a theorem/tactic that can explode the vector so I can rewrite with the inner nat, like below, so I can then use cbn
.
input: Vector.t nat 1
n: nat
Hin: input = [n]
==================================
complicated_fixpoint_for [n] = true
inversion input
does introduce n: nat
but surprisingly not Hin
, which does not help me call cbn
afterwards.