proposition: Lemma vint_typs_eq : forall n (Ts Us : Tys n) p (ts : Tes p), vint Us ts -> Us = Ts -> vint Ts ts.
proof: Proof. intros n Ts Us p ts h e. subst. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)