proposition: Lemma mi_eval_ok : forall f v, vec_invariant (mi_eval_aux (trsInt f) (Vmap dom2vec v)).
proof: Proof. intros. unfold vec_invariant, Conf.vec_at0. apply not_minusInf_ge_A1. set (w := mi_eval_at0). unfold vec_at0 in w. apply w. apply trsIntOk. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)