proposition: Lemma maxvars_cast : forall n (ts : terms n) p (e : n=p), maxvars (Vcast ts e) = maxvars ts.
proof: Proof. induction ts; destruct p; intros; try lia. rewrite Vcast_refl. refl. rewrite Vcast_cons, !maxvars_cons, IHts. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)