proposition: Lemma term_ge_incl_succeq : term_ge << IR_succeq.
proof: Proof. intros l r lr v. destruct (mint_eval_equiv l r v). simpl in * . unfold succeq, Rof. rewrite <- (vec_ge_mor H H0). apply mint_eval_mon_succeq. hyp. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)