proposition: Lemma size_non_zero : forall t, size t > 0.
proof: Proof. intro. pattern t. apply term_ind with (Q := fun n (ts : terms n) => size_terms ts >= 0); clear t. intro. simpl. lia. intros. rewrite size_fun. lia. simpl. lia. intros. simpl. lia. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)