fact: Definition term_ord (ord : forall n, relation (mint n)) l r := let (li, ri) := rule_mi (mkRule l r) in ord _ li ri.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)