proposition: Lemma mi_eval_ok : forall f v, vec_invariant (mi_eval_aux (trsInt f) (Vmap dom2vec v)).
proof: Proof. compute. trivial. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)