proposition: Theorem compFold_flatten : forall (A B C D: Set) P (eqd1 eqd2 : EqDec C)(c1 : C -> (D * list A) -> Comp C)(c2 : C -> B -> Comp C)(ls1 : list (D * (list A)))(ls2 : list B) init x, list_pred P (flatten (flatten_prep ls1)) ls2 -> (forall d lsa lsb init x, list_pred P (map (fun p => [i, a] <-2 p; (i, (length lsa), d, a)) (zip (allNatsLt (length lsa)) lsa)) lsb -> evalDist (c1 init (d, lsa)) x == evalDist (compFold eqd2 c2 init lsb) x) -> evalDist (compFold eqd1 c1 init ls1) x == evalDist (compFold eqd2 c2 init ls2) x.
proof: Proof. induction ls1; intuition. simpl in H. inversion H; clear H; subst. unfold compFold. eapply evalDist_ret_eq. trivial. simpl in H. unfold compFold. fold compFold. eapply list_pred_app in H. intuition. erewrite <- (@firstn_skipn _ _ ls2). rewrite compFold_app. comp_skip. Qed.
imports: FCF.FCF