fact: Definition getEquivMin (Ar1 Ar2 : rArray vM) (a : rNat) : rZ := match getEquiv Ar1 a with | (L1, true) => match getEquiv Ar2 a with | (L2, true) => match getMinId L1 L2 with | Some b => rZComp b | None => rZPlus zero end | (L2, false) => match getMinInv L1 L2 with | Some b => rZComp b | None => rZPlus zero end end | (L1, false) => match getEquiv Ar2 a with | (L2, true) => match getMinInv L1 L2 with | Some b => b | None => rZPlus zero end | (L2, false) => match getMinId L1 L2 with | Some b => b | None => rZPlus zero end end end.