proposition: Lemma cap_var_atom (a: Atom) b: e_var b ⊓ atom a ≡ (if set.mem a b then atom a else bot).
proof: Proof. generalize (in_seq b). unfold atom. induction (seq n). intros []. simpl (sup _ _). intros [->|Hl]. case set.mem. lattice. rewrite capA, capneg. apply capbx. rewrite capA, (capC (e_var _)), <-capA, IHl by assumption. case (set.mem a b). reflexivity. apply capxb. Qed.
imports: lattice lsyntax comparisons lset boolean sups