proposition: Lemma Vin_size_terms_gt : forall n (ts : terms n) t, Vin t ts -> n > 1 -> size_terms ts > size t.
proof: Proof. intro. destruct n. lia. destruct n. lia. intros. VSntac ts. rewrite H1 in H. VSntac (Vtail ts). rewrite H2 in H. simpl in *. ded (size_non_zero (Vhead ts)). ded (size_non_zero (Vhead (Vtail ts))). destruct H. subst t. lia. destruct H. subst t. lia. ded (Vin_size_terms_ge H). lia. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)