fact: Definition rule_mi r := let mvl := maxvar (lhs r) in let mvr := maxvar (rhs r) in let m := max mvl mvr in let lt := inject_term (Nat.le_max_l mvl mvr) in let rt := inject_term (Nat.le_max_r mvl mvr) in (mi_of_term lt, mi_of_term rt).
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)