fact: Fixpoint cmp A B := match A, B with | Base a, Base b => BCmp.cmp a b | Base _, Arr _ _ => Lt | Arr _ _, Base _ => Gt | Arr A1 A2, Arr B1 B2 => match cmp A1 B1 with | Eq => cmp A2 B2 | c => c end end.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)