fact: Definition vtl'' {A:Type}{n:nat}(v : t A n) : match n with 0 => t A 0 | S p => t A p end := match v in t _ n return match n with 0 => t A 0 | S p => t A p end with | nil _ => nil _ | cons _ a _ w => w end.
imports: Vector