proposition: Lemma fold_add_below x p i : ~In x p -> Below x p -> eqA (fold f (add x p) i) (fold f p (f x i)).
proof: Proof. intros Hxp Hxp' . apply (fold_4 equivalence_eqA _ Hcompat). repeat intro. apply Hxp'. auto. rewrite P.Add_Equal. reflexivity. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)