proposition: Lemma atom_xI n (f: ord (pow2 n)): @atom (S n) (set.xI f) ≡ e_var ord0 ⊓ eval (fun i => e_var (ordS i)) (atom f).
proof: Proof. unfold atom. simpl. rewrite set.mem_xI_0. apply cap_weq. reflexivity. setoid_rewrite eval_inf with (g := fun i => e_var (ordS i)). rewrite sup_map. apply (sup_weq (l:=BL) (L:=lattice.dual_laws _ _ _)). 2: reflexivity. intro i. rewrite set.mem_xI_S. now case set.mem. Qed.
imports: lattice lsyntax comparisons lset boolean sups