proposition: Theorem compMap_cons: forall (A : Type)(B : Set)(eqdb : EqDec B) (ls : list A)(c : A -> Comp B) (a : A) x, evalDist (compMap _ c (a :: ls)) x == evalDist (b <-$ c a; lsb <-$ compMap _ c ls; ret (b :: lsb)) x.
proof: Proof. intuition. simpl. intuition. Qed.
imports: FCF.FCF