fact: Fixpoint SumType {n} (v : Vector.t Type n) {struct v} : Type := match v with | Vector.nil => (False : Type) | Vector.cons T _ Vector.nil => T | Vector.cons T _ v' => T + (SumType v') end%type.
imports: Coq.Vectors.Vector Coq.Vectors.Vector Fiat.Common.BoundedLookup