proposition: Lemma eval_atom (a b: Atom): eval (set.mem a) (atom b) -> a=b.
proof: Proof. intro. apply set.ext. intro i. unfold atom in H. setoid_rewrite eval_inf with (g := set.mem a) in H. rewrite is_true_inf in H; cbv beta in H. specialize (H i (in_seq i)). destruct (set.mem b i). assumption. apply Bool.negb_true_iff. assumption. Qed.
imports: lattice lsyntax comparisons lset boolean sups