proposition: Theorem compFold_eq' : forall (A1 A2 : Set) P (ls1 : list A1) (ls2 : list A2), list_pred P ls1 ls2 -> forall (B : Set)(eqd1 eqd2 : EqDec B) (c1 : B -> A1 -> Comp B) (c2: B -> A2 -> Comp B), (forall acc a1 a2 x, P a1 a2 -> In a1 ls1 -> In a2 ls2 ->evalDist (c1 acc a1) x == evalDist (c2 acc a2) x) -> forall init x, evalDist (compFold eqd1 c1 init ls1) x == evalDist (compFold eqd2 c2 init ls2) x.
proof: Proof. induction 1; intuition. unfold compFold. eapply evalDist_ret_eq. intuition. unfold compFold. comp_skip. Qed.
imports: FCF.FCF Permutation