proposition: Lemma mint_eval_eq_term_int_var : forall v (val : valuation I) k (t_b : maxvar_le k (Var v)), dom2vec (bterm_int val (inject_term t_b)) =v mint_eval val (mi_of_term (inject_term t_b)).
proof: Proof. intros. rewrite mint_eval_split. change (const (mi_of_term (inject_term t_b))) with (zero_vec dim). rewrite vector_plus_zero_l. change (args (mi_of_term (inject_term t_b))) with (Vreplace (Vconst (zero_matrix dim dim) (S k)) (le_lt_S (maxvar_var t_b)) (id_matrix dim)). rewrite mint_eval_var_aux, Vbuild_nth. simpl. trans (col_mat_to_vec (vec_to_col_mat (dom2vec (val v)))). rewrite col_mat_to_vec_idem. refl. apply get_col_mor. rewrite mat_mult_id_l. refl. ded dim_pos. auto. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)