proposition: Lemma compFold_app : forall (A: Set)(B : Type)(eqd : EqDec A)(c : A -> B -> Comp A)(ls1 ls2 : list B) init x, evalDist (compFold _ c init (ls1 ++ ls2)) x == evalDist (init' <-$ compFold _ c init ls1; compFold _ c init' ls2) x.
proof: Proof. induction ls1; intuition. rewrite app_nil_l. unfold compFold. fold compFold. comp_simp. intuition. rewrite <- app_comm_cons. unfold compFold. fold compFold. inline_first. comp_skip. Qed.
imports: FCF.FCF