proposition: Lemma fold_empty : forall s (i: A), Equal s empty -> eqA (fold f s i) i.
proof: Proof. intros s i Hs. rewrite (fold_equal _ Hcompat _ Hs). rewrite Props.fold_empty. reflexivity. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)