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)