proposition: Lemma vint_forall_sn : forall n (Ts : Tys n) p (ts : Tes p), vint Ts ts -> Vforall (SN R_aeq) ts.
proof: Proof. induction Ts; destruct ts; simpl; auto. fo. intros [h1 h2]. split. eapply int_sn. apply h1. apply IHTs. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)