proposition: Lemma repeatMax_fold_in_support_false : forall (A B : Set)(ls : list B)(eqd : EqDec A)(c : B -> Comp A)(P : A -> bool)(a : A), (forall b, In b ls -> In a (getSupport (c b))) -> P a = false -> In a (getSupport (compFold eqd (fun (a' : A) b => if P a' then ret a' else (c b)) a ls)).
proof: Proof. induction ls; intuition. simpl. intuition. unfold compFold. fold compFold. eapply getSupport_In_Seq. rewrite H0. eapply H. simpl. intuition. eapply IHls; intuition. Qed.
imports: FCF.FCF