proposition: Lemma term_int_eq_restrict_lt : forall xint t k, maxvar t < k -> term_int xint t = term_int (restrict xint k) t.
proof: Proof. intros xint t. pattern t; apply term_ind_forall; clear t; intros. simpl. unfold restrict. case (le_lt_dec k v); intro. simpl in H. absurd (v<k); lia. refl. simpl. apply (f_equal (fint I f)). apply Vmap_eq. apply Vforall_intro. intros. apply (Vforall_in H H1). rewrite maxvar_fun in H0. ded (Vin_map_intro (f:=@maxvar Sig) H1). ded (Vmax_in H2). unfold maxvars in H0. lia. Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)