proposition: Lemma term_ind_comb : (forall t, Pt t) /\ (forall n (ts : terms n), Ps ts).
proof: Proof. split; [by apply term_ind with (Q := Ps) | intros n ts]. induction ts; [exact Hnil | apply Hcns; [idtac | hyp]]. by apply term_ind with (Q := Ps) . Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)