proposition: Lemma size_terms_app : forall n (ts : terms n) m (us : terms m), size_terms (Vapp ts us) = size_terms ts + size_terms us.
proof: Proof. induction ts; simpl; intros. refl. rewrite IHts. lia. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)