λ(m : Type) →
λ(partialLE : m → m → Bool) →
λ(a : m) →
λ(b : m) →
  partialLE a b && partialLE b a