Lexicographic ordering on lists (with functors)

Require Export DecOrders.

(* Lexicographic ordering for lists *)

Module List_Order (D: DEC_ORDER) <: DEC_ORDER with Definition
  A := list D.A .

Solution