proposition: Lemma var_fun1 : forall f u, var (Fun1 f u) = var u.
proof: Proof. intros. unfold Fun1, var; fold var. rewrite Vmap_first_cast. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)