proposition: Lemma vint_app_term_elim_r : forall n (Ts : Tys n) p (ts : Tes p) q (us : Tes q) (h : vint Ts (Vapp ts us)), vint (Vsub Ts (vint_le h)) us.
proof: Proof. intros n Ts p ts q us h. assert (a : p+q<=p+q). lia. rewrite <- Vsub_app_r with (v1:=ts) (h:=a). apply vint_sub_intro. hyp. refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)