proposition: Theorem decomp_top n: top ≡ e_top' n.
proof: Proof. unfold e_top'. induction n. symmetry. apply cupxb. simpl pow2. rewrite seq_double, sup_app. rewrite 2sup_map. setoid_rewrite atom_xO. setoid_rewrite atom_xI. rewrite <- 2capxsup. rewrite capC, (capC (e_var _)), <- capcup. rewrite cupC, cupneg, capxt. intros X L f. simpl. rewrite (IHn X L (fun i => f (ordS i))). rewrite 2eval_sup. apply sup_weq. 2: reflexivity. intro i. induction (atom i); first [reflexivity|apply cup_weq|apply cap_weq|apply neg_weq]; assumption. Qed.
imports: lattice lsyntax comparisons lset boolean sups