proposition: Lemma compMap_app : forall (A: Type)(B : Set)(eqd : EqDec B)(ls1 ls2 : list A)(c : A -> Comp B) x, evalDist (compMap _ c (ls1 ++ ls2)) x == evalDist (r1 <-$ compMap _ c ls1; r2 <-$ compMap _ c ls2; ret (r1 ++ r2)) x.
proof: Proof. induction ls1; intuition. rewrite app_nil_l. unfold compMap. fold compMap. comp_simp. rewrite <- evalDist_right_ident. comp_skip. simpl. reflexivity. rewrite <- app_comm_cons. unfold compMap. fold compMap. inline_first. comp_skip. eapply eqRat_trans. comp_skip. eapply eqRat_refl. inline_first. comp_skip. inline_first. comp_simp. comp_skip. simpl. intuition. Qed.
imports: FCF.FCF Permutation