proposition: Lemma Vin_nb_symb_occs_terms_ge : forall n (ts : terms n) t, Vin t ts -> nb_symb_occs_terms ts >= nb_symb_occs 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)