proposition: Lemma fun_eq : forall f v w, Fun f v = Fun f w -> v = w.
proof: Proof. intros. inversion H. apply (inj_existT (@eq_symb_dec _) H1). Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)