proposition: Lemma var_fill : forall c t, var (fill c t) = var t.
proof: Proof. induction c; simpl; intros. refl. rewrite Vmap_first_cast. arity. simpl. apply IHc. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)