let leq (l1: level) (l2: level) : bool =
match l1 with
| L -> true
| M (domain) -> (match l2 with
| L -> false
| M (domain') -> domain=domain'
| H -> true)
| H -> (match l2 with
L -> false
| M (domain) -> false
| H -> true)