proposition: Lemma mint_eval_eq_term_int t (val: valuation I) k (t_b: maxvar_le k t) : dom2vec (term_int val t) =v mint_eval val (mi_of_term (inject_term t_b)).
proof: Proof. intros. rewrite <- (term_int_eq_bterm_int val t_b). apply mint_eval_eq_bterm_int. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)