proposition: Theorem compMap_Q_eq_compFold : forall (B : Set)(eqdb : EqDec B)(Q : B -> bool) n1 (c : Comp B) z, Pr[ls <-$ compMap _ (fun _ => c) (forNats n1); ret (fold_left (fun b x => b || (Q x)) ls z)] == Pr[compFold _ (fun b _ => z <-$ (x <-$ c; ret Q x); ret b || z) z (forNats n1)].
proof: Proof. induction n1; intuition. simpl. comp_simp. simpl. intuition. Local Opaque evalDist. simpl. inline_first. comp_skip. inline_first. comp_simp. comp_at comp_ret leftc 1%nat. eapply IHn1. Qed.
imports: FCF.FCF Permutation