proposition: Lemma repeatMax_fold_true : forall (A B: Set)(ls : list B)(eqd : EqDec A)(c : B -> Comp A)(P : A -> bool)(a : A), P a = true -> comp_spec eq (compFold _ (fun acc b => if (P acc) then (ret acc) else (c b)) a ls) (ret a).
proof: Proof. induction ls; intuition; simpl. eapply comp_spec_eq_refl. rewrite H. prog_simp. intuition. Qed.
imports: FCF.FCF