fact: Definition listUncons {n : nat} (xs : SizedList A (S n)) : A * SizedList A n := let (vs, prf) := xs in (match vs return length vs = S n -> A * SizedList A n with | [] => fun hf => False_rect _ (Nat.neq_0_succ _ hf) | v :: vs' => fun Seq => pair v (MkSizedType vs' (Nat.succ_inj _ _ Seq)) end) prf.
imports: Coq(PeanoNat) Coq(Vector) Coq(List)