proposition: Theorem decomp_expr e: e ==_[BL] \sup_(i \in filter (fun f => eval (set.mem f) e) (seq (pow2 n))) atom i.
proof: Proof. rewrite <-capxt. setoid_rewrite decomp_top. setoid_rewrite capxsup. setoid_rewrite eval_mem_cap. induction (seq (pow2 n)). reflexivity. simpl filter. simpl (sup _ _). case (eval (set.mem a) e). now apply cup_weq. now rewrite cupbx. Qed.
imports: lattice lsyntax comparisons lset boolean sups