proposition: Lemma compFold_foldBodyOption_None : forall (A B : Set)(eqd : EqDec A)(c : A -> B -> Comp (option A))(ls : list B) x, evalDist (compFold _ (foldBody_option _ c) None ls) x == evalDist (ret None) x.
proof: Proof. induction ls; intuition. unfold compFold. intuition. unfold compFold. fold compFold. unfold foldBody_option. comp_simp. eapply IHls. Qed.
imports: FCF.FCF Permutation