proposition: Lemma term_ind_size : forall (P : term -> Prop), (forall n, (forall t, size t <= n -> P t) -> forall t, size t <= S n -> P t) -> forall t, P t.
proof: Proof. intro P. set (Q := fun n => forall t, size t <= n -> P t). change ((forall n, Q n -> Q (S n)) -> forall t, P t). intro IH. cut (forall t, Q t). intros. unfold Q in H. eapply H. apply Nat.le_refl. induction t. unfold Q. destruct t; simpl; intros; lia. apply IH. hyp. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)