proposition: Lemma Vin_size_terms_ge : forall n (ts : terms n) t, Vin t ts -> size_terms ts >= size t.
proof: Proof. induction ts; simpl; intros. contr. destruct H. subst h. lia. ded (IHts _ H). lia. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)