proposition: Lemma sub_fun1 : forall s f u, sub s (Fun1 f u) = Fun1 f (sub s u).
proof: Proof. intros. unfold Fun1. rewrite sub_fun, Vmap_cast. simpl Vmap. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)