fact: Definition u_lattice_ops := {| car := uexpr; leq := u_leq; weq := u_weq; cup := @e_pls _ _ _ _ _; bot := e_zer _ _; lattice.top := e_top _ _; cap := @e_cap _ _ _ _ _; neg := @e_neg _ _ _ _ _ |}.
imports: kleene syntax