proposition: Lemma term_int_eq_restrict : forall xint t, term_int xint t = term_int (restrict xint (maxvar t + 1)) t.
proof: Proof. intros. apply term_int_eq_restrict_lt. lia. Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)