proposition: Lemma term_gt_dec : rel_dec term_gt.
proof: Proof. intros l r. unfold term_gt, term_ord. simpl. match goal with |- {mint_gt ?l ?r} + {~mint_gt ?l ?r} => destruct (mint_gt_dec l r); auto end. Defined.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)