proposition: Lemma maxvar_fill : forall (t : term) c, maxvar (fill c t) = maxvar t.
proof: Proof. induction c. refl. simpl fill. rewrite maxvar_fun. unfold maxvars. rewrite Vmap_cast, Vmax_cast. arity. simpl. rewrite IHc. apply max_0_r. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)