fact: Fixpoint vint {n} (Ts : Tys n) {p} (ts : Tes p) := match Ts, ts with | _, Vnil => True | Vcons T Ts', Vcons t ts' => int T t /\ vint Ts' ts' | _, _ => False end.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)