fact: Parameter inv_id_matrix : vec_invariant (Vreplace (Vconst A0 dim) dim_pos A1).
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)