proposition: Lemma mint_eval_eq_bterm_int : forall (val : valuation I) t k (t_b : maxvar_le k t), dom2vec (bterm_int val (inject_term t_b)) =v mint_eval val (mi_of_term (inject_term t_b)).
proof: Proof. intros val t. pattern t. apply term_ind_forall; intros. apply mint_eval_eq_term_int_var. rewrite inject_term_eq. simpl. rewrite Vmap_map, (@Vforall2_map_intro _ _ eq_vec (fun x => dom2vec (bterm_int val x)) (fun (t : bterm k) => mint_eval val (mi_of_term t))). apply mint_eval_eq_bterm_int_fapp. apply Vforall_nth_intro. intros. rewrite inject_terms_nth. apply (Vforall_nth ip H). Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)