proposition: Lemma cup_var_atom (a: Atom) b: e_var b ⊔ !atom a ≡ (if set.mem a b then top else !atom a).
proof: Proof. generalize (in_seq b). unfold atom. induction (seq n). intros []. simpl (sup _ _). intros [->|Hl]. case set.mem. rewrite negcap, cupA, cupneg. apply cuptx. rewrite negcap, negneg. lattice. rewrite negcap at 1. rewrite cupA, (cupC (e_var _)), <-cupA, IHl by assumption. case (set.mem a b). apply cupxt. now rewrite negcap. Qed.
imports: lattice lsyntax comparisons lset boolean sups