proposition: Lemma exists_fold' : forall x init init', init = init' -> exists_ f x || init = fold (fun k acc => f k || acc) x init'.
proof: Proof. assert (Hf' : compat_op E.eq Logic.eq (fun k acc => f k || acc)). repeat intro. subst. rewrite (Hcompat _ _ H). reflexivity. induction x using set_induction_below; intros init init' Hinit. rewrite (fold_empty); auto with typeclass_instances. rewrite (exists_compat _ _ H). rewrite Hinit. rewrite (exists_empty). reflexivity. rewrite (fold_equal _ Hf' _ H1). rewrite (fold_add_below ); auto with typeclass_instances. rewrite (exists_compat _ _ H1). rewrite (exists_add _ _ H). rewrite <- orb_assoc. rewrite (@IHx1 (f x2 || init) (f x2 || init')). reflexivity. subst; reflexivity. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)