proposition: Lemma empty_atom_cap (a b: Atom): a<>b -> atom a ⊓ atom b ≡ bot.
proof: Proof. intro E. rewrite eval_mem_cap. generalize (eval_atom b a). case (eval (set.mem b) (atom a)). 2: reflexivity. intro. elim E. symmetry; auto. Qed.
imports: lattice lsyntax comparisons lset boolean sups