proposition: Lemma mint_eval_equiv : forall l r (val : valuation I), let (li, ri) := rule_mi (mkRule l r) in let lev := term_int val l in let rev := term_int val r in let lv := mint_eval val li in let rv := mint_eval val ri in lv =v dom2vec lev /\ rv =v dom2vec rev.
proof: Proof. intros. simpl. split. rewrite (mint_eval_eq_term_int val (Nat.le_max_l (maxvar l) (maxvar r))). refl. rewrite (mint_eval_eq_term_int val (Nat.le_max_r (maxvar l) (maxvar r))). refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)